let R be comRing; :: thesis: for M being LeftMod of R
for f being Endomorphism of R,M st f = 1_End M holds
AbGr f = 1_End (AbGr M)
let M be LeftMod of R; :: thesis: for f being Endomorphism of R,M st f = 1_End M holds
AbGr f = 1_End (AbGr M)
let f be Endomorphism of R,M; :: thesis: ( f = 1_End M implies AbGr f = 1_End (AbGr M) )
assume f = 1_End M ; :: thesis: AbGr f = 1_End (AbGr M)
then AbGr f = id (AbGr M) by Def26;
hence AbGr f = 1_End (AbGr M) ; :: thesis: verum