let R be comRing; :: thesis: for M, N being LeftMod of R
for f, g being Homomorphism of R,M,N holds
( f in Funcs ( the carrier of M, the carrier of N) & g in Funcs ( the carrier of M, the carrier of N) & (add_Hom (M,N)) . [f,g] = (ADD (M,N)) . (f,g) & (ADD (M,N)) . (f,g) is Homomorphism of R,M,N )
let M, N be LeftMod of R; :: thesis: for f, g being Homomorphism of R,M,N holds
( f in Funcs ( the carrier of M, the carrier of N) & g in Funcs ( the carrier of M, the carrier of N) & (add_Hom (M,N)) . [f,g] = (ADD (M,N)) . (f,g) & (ADD (M,N)) . (f,g) is Homomorphism of R,M,N )
let f, g be Homomorphism of R,M,N; :: thesis: ( f in Funcs ( the carrier of M, the carrier of N) & g in Funcs ( the carrier of M, the carrier of N) & (add_Hom (M,N)) . [f,g] = (ADD (M,N)) . (f,g) & (ADD (M,N)) . (f,g) is Homomorphism of R,M,N )
( f in set_Hom (M,N) & g in set_Hom (M,N) ) ;
hence ( f in Funcs ( the carrier of M, the carrier of N) & g in Funcs ( the carrier of M, the carrier of N) & (add_Hom (M,N)) . [f,g] = (ADD (M,N)) . (f,g) & (ADD (M,N)) . (f,g) is Homomorphism of R,M,N ) by ZFMISC_1:87, FUNCT_1:49, Th18; :: thesis: verum