let R be comRing; :: thesis: for M being LeftMod of R
for f, g, h being Endomorphism of R,M st h = (ADD (M,M)) . (f,g) holds
AbGr h = (ADD ((AbGr M),(AbGr M))) . ((AbGr f),(AbGr g))
let M be LeftMod of R; :: thesis: for f, g, h being Endomorphism of R,M st h = (ADD (M,M)) . (f,g) holds
AbGr h = (ADD ((AbGr M),(AbGr M))) . ((AbGr f),(AbGr g))
let f, g, h be Endomorphism of R,M; :: thesis: ( h = (ADD (M,M)) . (f,g) implies AbGr h = (ADD ((AbGr M),(AbGr M))) . ((AbGr f),(AbGr g)) )
assume A1: h = (ADD (M,M)) . (f,g) ; :: thesis: AbGr h = (ADD ((AbGr M),(AbGr M))) . ((AbGr f),(AbGr g))
reconsider f1 = AbGr f, g1 = AbGr g as Element of Funcs ( the carrier of (AbGr M), the carrier of (AbGr M)) by FUNCT_2:8;
reconsider f0 = f, g0 = g, h0 = h as Element of Funcs ( the carrier of M, the carrier of M) by FUNCT_2:8;
for x being Element of the carrier of (AbGr M) holds (AbGr h) . x = ((AbGr f) . x) + ((AbGr g) . x)

proof

let x be Element of the carrier of (AbGr M); :: thesis: (AbGr h) . x = ((AbGr f) . x) + ((AbGr g) . x)
reconsider x0 = x as Element of the carrier of M ;
A2: (AbGr f) . x = f . x0 by Def26;
A3: (AbGr g) . x = g . x0 by Def26;
A4: (AbGr h) . x = h . x0 by Def26;
(AbGr h) . x = h0 . x0 by A4
.= (f0 . x0) + (g0 . x0) by A1, Th15
.= ((AbGr f) . x) + ((AbGr g) . x) by A2, A3 ;
hence (AbGr h) . x = ((AbGr f) . x) + ((AbGr g) . x) ; :: thesis: verum

end;

hence AbGr h = (ADD ((AbGr M),(AbGr M))) . ((AbGr f),(AbGr g)) by Th30; :: thesis: verum