:: deftheorem Def23 defines tau LMOD_XX1:def 23 :
for R being comRing
for M1, M, N being LeftMod of R
for u being Homomorphism of R,M1,M
for b₆ being Function of (Hom (R,M,N)),(Hom (R,M1,N)) holds
( b₆ = tau (N,u) iff for f being Element of (Hom (R,M,N)) ex f1 being Homomorphism of R,M,N st
( f = f1 & b₆ . f = f1 * u ) );