let g1, g2 be Function of R,(End_Ring (AbGr M)); :: thesis: ( ( for x being object st x in the carrier of R holds
ex f being Endomorphism of R,M st
( f = (curry the lmult of M) . x & g1 . x = AbGr f ) ) & ( for x being object st x in the carrier of R holds
ex f being Endomorphism of R,M st
( f = (curry the lmult of M) . x & g2 . x = AbGr f ) ) implies g1 = g2 )
assume that
A6: for x being object st x in the carrier of R holds
ex f1 being Endomorphism of R,M st
( f1 = (curry the lmult of M) . x & g1 . x = AbGr f1 ) and
A7: for x being object st x in the carrier of R holds
ex f2 being Endomorphism of R,M st
( f2 = (curry the lmult of M) . x & g2 . x = AbGr f2 ) ; :: thesis: g1 = g2
A8: dom g1 = the carrier of R by FUNCT_2:def 1
.= dom g2 by FUNCT_2:def 1 ;

now :: thesis: for x being object st x in dom g1 holds
g1 . x = g2 . x

let x be object ; :: thesis: ( x in dom g1 implies g1 . x = g2 . x )
assume A9: x in dom g1 ; :: thesis: g1 . x = g2 . x
then consider f1 being Endomorphism of R,M such that
A10: f1 = (curry the lmult of M) . x and
A11: g1 . x = AbGr f1 by A6;
consider f2 being Endomorphism of R,M such that
A12: f2 = (curry the lmult of M) . x and
A13: g2 . x = AbGr f2 by A7, A9;
thus g1 . x = g2 . x by A13, A11, A12, A10; :: thesis: verum

end;

hence g1 = g2 by A8; :: thesis: verum