defpred S₁[ object , object ] means ex a, s being Element of A st
( s in S & $1 = Class ((EqRel S),[a,s]) & $2 = (f . a) * ((f . s) ["]) );
A2: for x being object st x in the carrier of (S ~ A) holds
ex y being object st
( y in the carrier of B & S₁[x,y] )

proof

let x be object ; :: thesis: ( x in the carrier of (S ~ A) implies ex y being object st
( y in the carrier of B & S₁[x,y] ) )
assume x in the carrier of (S ~ A) ; :: thesis: ex y being object st
( y in the carrier of B & S₁[x,y] )
then reconsider z = x as Element of (S ~ A) ;
consider a, s being Element of A such that
A4: s in S and
A5: z = Class ((EqRel S),[a,s]) by Th46;
reconsider y = (f . a) * ((f . s) ["]) as Element of B ;
S₁[x,y] by A4, A5;
hence ex y being object st
( y in the carrier of B & S₁[x,y] ) ; :: thesis: verum

end;

ex g being Function of (S ~ A),B st
for x being object st x in the carrier of (S ~ A) holds
S₁[x,g . x] from FUNCT_2:sch 1(A2);
then consider g being Function of (S ~ A),B such that
A6: for x being object st x in the carrier of (S ~ A) holds
ex a, s being Element of A st
( s in S & x = Class ((EqRel S),[a,s]) & g . x = (f . a) * ((f . s) ["]) ) ;
take g ; :: thesis: for x being object st x in the carrier of (S ~ A) holds
ex a, s being Element of A st
( s in S & x = Class ((EqRel S),[a,s]) & g . x = (f . a) * ((f . s) ["]) )
thus for x being object st x in the carrier of (S ~ A) holds
ex a, s being Element of A st
( s in S & x = Class ((EqRel S),[a,s]) & g . x = (f . a) * ((f . s) ["]) ) by A6; :: thesis: verum