let R be comRing; :: thesis: for M, N being LeftMod of R
for a being Element of R
for f1 being Element of (Func_Mod (R,M,N))
for f being Element of (Hom (R,M,N)) st f1 = f holds
a * f = a * f1
let M, N be LeftMod of R; :: thesis: for a being Element of R
for f1 being Element of (Func_Mod (R,M,N))
for f being Element of (Hom (R,M,N)) st f1 = f holds
a * f = a * f1
let a be Element of R; :: thesis: for f1 being Element of (Func_Mod (R,M,N))
for f being Element of (Hom (R,M,N)) st f1 = f holds
a * f = a * f1
let f1 be Element of (Func_Mod (R,M,N)); :: thesis: for f being Element of (Hom (R,M,N)) st f1 = f holds
a * f = a * f1
let f be Element of (Hom (R,M,N)); :: thesis: ( f1 = f implies a * f = a * f1 )
assume A1: f1 = f ; :: thesis: a * f = a * f1
reconsider f0 = f as Homomorphism of R,M,N by Lm29;
a * f = (LMULT (M,N)) . (a,f0) by Th22
.= a * f1 by A1 ;
hence a * f = a * f1 ; :: thesis: verum