let R be comRing; :: thesis: for M being LeftMod of R
for f, g, h being Endomorphism of R,M holds
( AbGr h = (FuncComp (AbGr M)) . ((AbGr f),(AbGr g)) iff for x being Element of the carrier of (AbGr M) holds (AbGr h) . x = ((AbGr f) * (AbGr g)) . x )
let M be LeftMod of R; :: thesis: for f, g, h being Endomorphism of R,M holds
( AbGr h = (FuncComp (AbGr M)) . ((AbGr f),(AbGr g)) iff for x being Element of the carrier of (AbGr M) holds (AbGr h) . x = ((AbGr f) * (AbGr g)) . x )
let f, g, h be Endomorphism of R,M; :: thesis: ( AbGr h = (FuncComp (AbGr M)) . ((AbGr f),(AbGr g)) iff for x being Element of the carrier of (AbGr M) holds (AbGr h) . x = ((AbGr f) * (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 = (FuncComp (AbGr M)) . ((AbGr f),(AbGr g)) implies for x being Element of the carrier of (AbGr M) holds (AbGr h) . x = ((AbGr f) * (AbGr g)) . x ) :: thesis: ( ( for x being Element of the carrier of (AbGr M) holds (AbGr h) . x = ((AbGr f) * (AbGr g)) . x ) implies AbGr h = (FuncComp (AbGr M)) . ((AbGr f),(AbGr g)) )

proof

assume AbGr h = (FuncComp (AbGr M)) . ((AbGr f),(AbGr g)) ; :: thesis: for x being Element of the carrier of (AbGr M) holds (AbGr h) . x = ((AbGr f) * (AbGr g)) . x
then for x being Element of the carrier of (AbGr M) holds h1 . x = (f1 * g1) . x by Def4;
hence for x being Element of the carrier of (AbGr M) holds (AbGr h) . x = ((AbGr f) * (AbGr g)) . x ; :: thesis: verum

end;

assume A3: for x being Element of the carrier of (AbGr M) holds (AbGr h) . x = ((AbGr f) * (AbGr g)) . x ; :: thesis: AbGr h = (FuncComp (AbGr M)) . ((AbGr f),(AbGr g))
AbGr h = (FuncComp (AbGr M)) . ((AbGr f),(AbGr g))

proof

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

proof

let x be Element of the carrier of (AbGr M); :: thesis: (AbGr h) . x = ((FuncComp (AbGr M)) . ((AbGr f),(AbGr g))) . x
((FuncComp (AbGr M)) . (f1,g1)) . x = (f1 * g1) . x by Def4
.= h1 . x by A3 ;
hence (AbGr h) . x = ((FuncComp (AbGr M)) . ((AbGr f),(AbGr g))) . x ; :: thesis: verum

end;

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

end;

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