let R be comRing; :: thesis: for M, N, N1 being LeftMod of R
for f, g being Element of Funcs ( the carrier of M, the carrier of N)
for u being Element of Funcs ( the carrier of N, the carrier of N1) st u is additive holds
u * ((ADD (M,N)) . (f,g)) = (ADD (M,N1)) . ((u * f),(u * g))
let M, N, N1 be LeftMod of R; :: thesis: for f, g being Element of Funcs ( the carrier of M, the carrier of N)
for u being Element of Funcs ( the carrier of N, the carrier of N1) st u is additive holds
u * ((ADD (M,N)) . (f,g)) = (ADD (M,N1)) . ((u * f),(u * g))
let f, g be Element of Funcs ( the carrier of M, the carrier of N); :: thesis: for u being Element of Funcs ( the carrier of N, the carrier of N1) st u is additive holds
u * ((ADD (M,N)) . (f,g)) = (ADD (M,N1)) . ((u * f),(u * g))
let u be Element of Funcs ( the carrier of N, the carrier of N1); :: thesis: ( u is additive implies u * ((ADD (M,N)) . (f,g)) = (ADD (M,N1)) . ((u * f),(u * g)) )
assume A1: u is additive ; :: thesis: u * ((ADD (M,N)) . (f,g)) = (ADD (M,N1)) . ((u * f),(u * g))
reconsider fg = (ADD (M,N)) . (f,g) as Element of Funcs ( the carrier of M, the carrier of N) ;
reconsider uf = u * f as Element of Funcs ( the carrier of M, the carrier of N1) ;
reconsider ug = u * g as Element of Funcs ( the carrier of M, the carrier of N1) ;
for x being Element of the carrier of M holds (u * fg) . x = ((ADD (M,N1)) . (uf,ug)) . x

proof

let x be Element of the carrier of M; :: thesis: (u * fg) . x = ((ADD (M,N1)) . (uf,ug)) . x
A2: ( uf . x = u . (f . x) & ug . x = u . (g . x) ) by FUNCT_2:15;
reconsider fx = f . x, gx = g . x as Element of the carrier of N ;
(u * fg) . x = u . (((ADD (M,N)) . (f,g)) . x) by FUNCT_2:15
.= u . ((f . x) + (g . x)) by Th15
.= (uf . x) + (ug . x) by A1, A2
.= ((ADD (M,N1)) . (uf,ug)) . x by Th15 ;
hence (u * fg) . x = ((ADD (M,N1)) . (uf,ug)) . x ; :: thesis: verum

end;

hence u * ((ADD (M,N)) . (f,g)) = (ADD (M,N1)) . ((u * f),(u * g)) ; :: thesis: verum