defpred S₁[ set , set ] means ex f being Function st
( $1 = f & $2 = commute f );
A1: for x, y1, y2 being set st S₁[x,y1] & S₁[x,y2] holds
y1 = y2 ;
consider X being set such that
A2: for x being set holds
( x in X iff ex y being set st
( y in dom F & S₁[y,x] ) ) from TARSKI:sch 1(A1);
defpred S₂[ set , set ] means for f being Function st $1 = f holds
$2 = F . (commute f);

A3: now

let x be set ; :: thesis: ( x in X implies ex y being set st S₂[x,y] )
assume x in X ; :: thesis: ex y being set st S₂[x,y]
then ex y being set st
( y in dom F & ex f being Function st
( y = f & x = commute f ) ) by A2;
then reconsider f = x as Function ;
take y = F . (commute f); :: thesis: S₂[x,y]
thus S₂[x,y] ; :: thesis: verum

end;

consider G being Function such that
A4: dom G = X and
A5: for x being set st x in X holds
S₂[x,G . x] from CLASSES1:sch 1(A3);
take G ; :: thesis: ( ( for x being set holds
( x in dom G iff ex f being Function st
( f in dom F & x = commute f ) ) ) & ( for f being Function st f in dom G holds
G . f = F . (commute f) ) )

hereby :: thesis: for f being Function st f in dom G holds
G . f = F . (commute f)

let x be set ; :: thesis: ( ( x in dom G implies ex f being Function st
( f in dom F & x = commute f ) ) & ( ex f being Function st
( f in dom F & x = commute f ) implies x in dom G ) )

hereby :: thesis: ( ex f being Function st
( f in dom F & x = commute f ) implies x in dom G )

assume x in dom G ; :: thesis: ex f being Function st
( f in dom F & x = commute f )
then consider y being set such that
A6: y in dom F and
A7: ex f being Function st
( y = f & x = commute f ) by A2, A4;
reconsider f = y as Function by A7;
take f = f; :: thesis: ( f in dom F & x = commute f )
thus ( f in dom F & x = commute f ) by A6, A7; :: thesis: verum

end;

thus ( ex f being Function st
( f in dom F & x = commute f ) implies x in dom G ) by A2, A4; :: thesis: verum

end;

thus for f being Function st f in dom G holds
G . f = F . (commute f) by A4, A5; :: thesis: verum