let R be comRing; :: thesis: for M, N, M1 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 M1, the carrier of M) holds ((ADD (M,N)) . (f,g)) * u = (ADD (M1,N)) . ((f * u),(g * u))
let M, N, M1 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 M1, the carrier of M) holds ((ADD (M,N)) . (f,g)) * u = (ADD (M1,N)) . ((f * u),(g * u))
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 M1, the carrier of M) holds ((ADD (M,N)) . (f,g)) * u = (ADD (M1,N)) . ((f * u),(g * u))
let u be Element of Funcs ( the carrier of M1, the carrier of M); :: thesis: ((ADD (M,N)) . (f,g)) * u = (ADD (M1,N)) . ((f * u),(g * u))
reconsider fg = (ADD (M,N)) . (f,g) as Element of Funcs ( the carrier of M, the carrier of N) ;
reconsider fu = f * u, gu = g * u as Element of Funcs ( the carrier of M1, the carrier of N) ;
for x being Element of the carrier of M1 holds (fg * u) . x = ((ADD (M1,N)) . (fu,gu)) . x

proof

let x be Element of the carrier of M1; :: thesis: (fg * u) . x = ((ADD (M1,N)) . (fu,gu)) . x
A1: ( fu . x = f . (u . x) & gu . x = g . (u . x) ) by FUNCT_2:15;
reconsider ux = u . x as Element of the carrier of M ;
(fg * u) . x = fg . ux by FUNCT_2:15
.= (fu . x) + (gu . x) by A1, Th15
.= ((ADD (M1,N)) . (fu,gu)) . x by Th15 ;
hence (fg * u) . x = ((ADD (M1,N)) . (fu,gu)) . x ; :: thesis: verum

end;

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