:: deftheorem Def24 defines phi LMOD_XX1:def 24 :
for R being comRing
for M, N, N1 being LeftMod of R
for u being Homomorphism of R,N,N1
for b6 being Function of (Hom (R,M,N)),(Hom (R,M,N1)) holds
( b6 = phi (M,u) iff for f being Element of (Hom (R,M,N)) ex f1 being Homomorphism of R,M,N st
( f = f1 & b6 . f = u * f1 ) );