let M be AbGroup; :: thesis: End_Ring M is well-unital
for f being Element of (End_Ring M) holds
( f * (1. (End_Ring M)) = f & (1. (End_Ring M)) * f = f )

proof

let f be Element of (End_Ring M); :: thesis: ( f * (1. (End_Ring M)) = f & (1. (End_Ring M)) * f = f )
f in set_End M ;
then consider f1 being Function of the carrier of M, the carrier of M such that
A1: ( f1 = f & f1 is Endomorphism of M ) ;
reconsider f1 = f1 as Element of Funcs ( the carrier of M, the carrier of M) by FUNCT_2:9;
reconsider I1 = id M as Element of Funcs ( the carrier of M, the carrier of M) by FUNCT_2:9;
A2: for x being Element of the carrier of M holds
( ((FuncComp M) . (f1,I1)) . x = f1 . x & ((FuncComp M) . (I1,f1)) . x = f1 . x )

proof

let x be Element of the carrier of M; :: thesis: ( ((FuncComp M) . (f1,I1)) . x = f1 . x & ((FuncComp M) . (I1,f1)) . x = f1 . x )
A3: ((FuncComp M) . (f1,I1)) . x = (f1 * I1) . x by Def4
.= f1 . (I1 . x) by FUNCT_2:15
.= f1 . x ;
((FuncComp M) . (I1,f1)) . x = (I1 * f1) . x by Def4
.= I1 . (f1 . x) by FUNCT_2:15
.= f1 . x ;
hence ( ((FuncComp M) . (f1,I1)) . x = f1 . x & ((FuncComp M) . (I1,f1)) . x = f1 . x ) by A3; :: thesis: verum

end;

A4: f * (1. (End_Ring M)) = (FuncComp M) . (f1,I1) by A1, Th6
.= f1 by A2
.= f by A1 ;
(1. (End_Ring M)) * f = (FuncComp M) . (I1,f1) by A1, Th6
.= f1 by A2
.= f by A1 ;
hence ( f * (1. (End_Ring M)) = f & (1. (End_Ring M)) * f = f ) by A4; :: thesis: verum

end;

hence End_Ring M is well-unital ; :: thesis: verum