let M be AbGroup; :: thesis: for f being object st f in set_End M holds
f is Endomorphism of M
let f be object ; :: thesis: ( f in set_End M implies f is Endomorphism of M )
assume f in set_End M ; :: thesis: f is Endomorphism of M
then consider f1 being Function of M,M such that
A2: ( f1 = f & f1 is Endomorphism of M ) ;
thus f is Endomorphism of M by A2; :: thesis: verum