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

proof

assume A2: AbGr h = (ADD ((AbGr M),(AbGr M))) . ((AbGr f),(AbGr g)) ; :: thesis: for x being Element of the carrier of (AbGr M) holds (AbGr h) . x = ((AbGr f) . x) + ((AbGr g) . x)
for x being Element of (AbGr M) holds (AbGr h) . x = ((AbGr f) . x) + ((AbGr g) . x)

proof

let x be Element of (AbGr M); :: thesis: (AbGr h) . x = ((AbGr f) . x) + ((AbGr g) . x)
A3: x in dom ( the addF of (AbGr M) .: (f1,g1)) by Lm1;
h1 . x = ( the addF of (AbGr M) .: (f1,g1)) . x by A2, Def1
.= (f1 . x) + (g1 . x) by A3, FUNCOP_1:22 ;
hence (AbGr h) . x = ((AbGr f) . x) + ((AbGr g) . x) ; :: thesis: verum

end;

hence for x being Element of the carrier of (AbGr M) holds (AbGr h) . x = ((AbGr f) . x) + ((AbGr g) . x) ; :: thesis: verum

end;

assume A4: for x being Element of the carrier of (AbGr M) holds (AbGr h) . x = ((AbGr f) . x) + ((AbGr g) . x) ; :: thesis: AbGr h = (ADD ((AbGr M),(AbGr M))) . ((AbGr f),(AbGr g))
AbGr h = (ADD ((AbGr M),(AbGr M))) . ((AbGr f),(AbGr g))

proof

A5: for x being Element of the carrier of (AbGr M) holds (AbGr h) . x = ((ADD ((AbGr M),(AbGr M))) . ((AbGr f),(AbGr g))) . x

proof

let x be Element of the carrier of (AbGr M); :: thesis: (AbGr h) . x = ((ADD ((AbGr M),(AbGr M))) . ((AbGr f),(AbGr g))) . x
A6: x in dom ( the addF of (AbGr M) .: (f1,g1)) by Lm1;
((ADD ((AbGr M),(AbGr M))) . (f1,g1)) . x = ( the addF of (AbGr M) .: (f1,g1)) . x by Def1
.= (f1 . x) + (g1 . x) by A6, FUNCOP_1:22
.= h1 . x by A4 ;
hence (AbGr h) . x = ((ADD ((AbGr M),(AbGr M))) . ((AbGr f),(AbGr g))) . x ; :: thesis: verum

end;

reconsider h2 = AbGr h, addfg2 = (ADD ((AbGr M),(AbGr M))) . (f1,g1) as Function of the carrier of (AbGr M), the carrier of (AbGr M) ;
h2 = addfg2 by A5;
hence AbGr h = (ADD ((AbGr M),(AbGr M))) . ((AbGr f),(AbGr g)) ; :: thesis: verum

end;

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