Hom commuting with tensor

Hom(M,N)*B=Hom(M_B,N_B) was first proved in Free,...

It was then used in Regular Sequences to prove Ext and Tor versions.

It was proved again in Extensions along with naturalness.

Hom_B(M*N,P)=Hom_A(M,Hom_B(N,P)) was first proved in Extensions in the context of bimodule theory, but (not its naturalness). It will be proved again in Bruns, along with naturalness in bimodule theory.

Edit: naturalness seems to be proved in Extension, not in Bruns.