defpred S₁[ object , object ] means ex f1 being Endomorphism of R,M st
( f1 = (curry the lmult of M) . $1 & $2 = AbGr f1 );
A1: for x being object st x in the carrier of R holds
ex y being object st
( y in the carrier of (End_Ring (AbGr M)) & S₁[x,y] )

proof

let x be object ; :: thesis: ( x in the carrier of R implies ex y being object st
( y in the carrier of (End_Ring (AbGr M)) & S₁[x,y] ) )
assume x in the carrier of R ; :: thesis: ex y being object st
( y in the carrier of (End_Ring (AbGr M)) & S₁[x,y] )
then reconsider x = x as Element of R ;
reconsider f1 = (curry the lmult of M) . x as Endomorphism of R,M by Th33;
AbGr f1 is Endomorphism of (AbGr M) by Th28;
then AbGr f1 in End_Ring (AbGr M) ;
then consider y being object such that
A3: y = AbGr f1 and
A4: y in End_Ring (AbGr M) ;
thus ex y being object st
( y in the carrier of (End_Ring (AbGr M)) & S₁[x,y] ) by A3, A4; :: thesis: verum

end;

ex g being Function of R,(End_Ring (AbGr M)) st
for x being object st x in the carrier of R holds
S₁[x,g . x] from FUNCT_2:sch 1(A1);
then consider g being Function of R,(End_Ring (AbGr M)) such that
A5: 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 & g . x = AbGr f1 ) ;
take g ; :: 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 & g . x = AbGr f )
thus 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 & g . x = AbGr f ) by A5; :: thesis: verum