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

proof

let x be object ; :: thesis: ( x in the carrier of (AbGr M) implies ex y being object st
( y in the carrier of (AbGr N) & S₁[x,y] ) )
assume x in the carrier of (AbGr M) ; :: thesis: ex y being object st
( y in the carrier of (AbGr N) & S₁[x,y] )
then reconsider z = x as Element of M ;
ex y being object st
( y in the carrier of (AbGr N) & y = f . z ) ;
hence ex y being object st
( y in the carrier of (AbGr N) & S₁[x,y] ) ; :: thesis: verum

end;

ex g being Function of (AbGr M),(AbGr N) st
for x being object st x in the carrier of (AbGr M) holds
S₁[x,g . x] from FUNCT_2:sch 1(A1);
then consider g being Function of (AbGr M),(AbGr N) such that
A4: for x being object st x in the carrier of (AbGr M) holds
g . x = f . x ;
take g ; :: thesis: for x being object st x in the carrier of (AbGr M) holds
g . x = f . x
thus for x being object st x in the carrier of (AbGr M) holds
g . x = f . x by A4; :: thesis: verum