let M be AbGroup; :: thesis: End_Ring M is right_zeroed
for f being Element of (End_Ring M) holds (add_End M) . (f,(0_End M)) = f

proof

let f be Element of (End_Ring M); :: thesis: (add_End M) . (f,(0_End M)) = 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 = f, z1 = 0_End M as Endomorphism of M by A1;
reconsider f1 = f1, z1 = z1 as Element of Funcs ( the carrier of M, the carrier of M) by Th3;
thus (add_End M) . (f,(0_End M)) = (ADD (M,M)) . (f1,z1) by Th3
.= f by Lm4 ; :: thesis: verum

end;

hence End_Ring M is right_zeroed ; :: thesis: verum