let R be comRing; :: thesis: for M, N being LeftMod of R
for f1, g1 being Element of (Func_Mod (R,M,N))
for f, g being Element of (Hom (R,M,N)) st f1 = f & g1 = g holds
f + g = f1 + g1
let M, N be LeftMod of R; :: thesis: for f1, g1 being Element of (Func_Mod (R,M,N))
for f, g being Element of (Hom (R,M,N)) st f1 = f & g1 = g holds
f + g = f1 + g1
let f1, g1 be Element of (Func_Mod (R,M,N)); :: thesis: for f, g being Element of (Hom (R,M,N)) st f1 = f & g1 = g holds
f + g = f1 + g1
let f, g be Element of (Hom (R,M,N)); :: thesis: ( f1 = f & g1 = g implies f + g = f1 + g1 )
assume A1: ( f1 = f & g1 = g ) ; :: thesis: f + g = f1 + g1
reconsider f0 = f as Homomorphism of R,M,N by Lm29;
reconsider g0 = g as Homomorphism of R,M,N by Lm29;
f + g = (ADD (M,N)) . (f0,g0) by Th21
.= f1 + g1 by A1 ;
hence f + g = f1 + g1 ; :: thesis: verum