let R be comRing; :: thesis: for M, N being LeftMod of R
for f being object holds
( f in set_Hom (M,N) iff f is Homomorphism of R,M,N )
let M, N be LeftMod of R; :: thesis: for f being object holds
( f in set_Hom (M,N) iff f is Homomorphism of R,M,N )
let f be object ; :: thesis: ( f in set_Hom (M,N) iff f is Homomorphism of R,M,N )
( f in set_Hom (M,N) implies f is Homomorphism of R,M,N )

proof

assume f in set_Hom (M,N) ; :: thesis: f is Homomorphism of R,M,N
then consider f1 being Function of M,N such that
A3: ( f1 = f & f1 is Homomorphism of R,M,N ) ;
thus f is Homomorphism of R,M,N by A3; :: thesis: verum

end;

hence ( f in set_Hom (M,N) iff f is Homomorphism of R,M,N ) ; :: thesis: verum