defpred S₁[ set ] means ex y being set st [$1,y] in dom f;
consider D1 being set such that
A1: for x being set holds
( x in D1 iff ( x in union (union (dom f)) & S₁[x] ) ) from XBOOLE_0:sch 1();
defpred S₂[ set ] means ex y being set st [y,$1] in dom f;
consider D2 being set such that
A2: for y being set holds
( y in D2 iff ( y in union (union (dom f)) & S₂[y] ) ) from XBOOLE_0:sch 1();
defpred S₃[ set ] means ex y, z being set st
( $1 = [z,y] & [y,z] in dom f );
consider D being set such that
A3: for x being set holds
( x in D iff ( x in [:D2,D1:] & S₃[x] ) ) from XBOOLE_0:sch 1();
defpred S₄[ set , set ] means ex y, z being set st
( $1 = [z,y] & $2 = f . [y,z] );
A4: for x, y1, y2 being set st x in D & S₄[x,y1] & S₄[x,y2] holds
y1 = y2

proof

let x, y1, y2 be set ; :: thesis: ( x in D & S₄[x,y1] & S₄[x,y2] implies y1 = y2 )
assume x in D ; :: thesis: ( not S₄[x,y1] or not S₄[x,y2] or y1 = y2 )
given y, z being set such that A5: x = [z,y] and
A6: y1 = f . [y,z] ; :: thesis: ( not S₄[x,y2] or y1 = y2 )
given y', z' being set such that A7: x = [z',y'] and
A8: y2 = f . [y',z'] ; :: thesis: y1 = y2
( z = z' & y = y' ) by A5, A7, ZFMISC_1:33;
hence y1 = y2 by A6, A8; :: thesis: verum

end;

A9: for x being set st x in D holds
ex y1 being set st S₄[x,y1]

proof

let x be set ; :: thesis: ( x in D implies ex y1 being set st S₄[x,y1] )
assume x in D ; :: thesis: ex y1 being set st S₄[x,y1]
then consider y, z being set such that
A10: x = [z,y] and
[y,z] in dom f by A3;
take f . [y,z] ; :: thesis: S₄[x,f . [y,z]]
thus S₄[x,f . [y,z]] by A10; :: thesis: verum

end;

consider h being Function such that
A11: dom h = D and
A12: for x being set st x in D holds
S₄[x,h . x] from FUNCT_1:sch 2(A4, A9);
take h ; :: thesis: ( ( for x being set holds
( x in dom h iff ex y, z being set st
( x = [z,y] & [y,z] in dom f ) ) ) & ( for y, z being set st [y,z] in dom f holds
h . z,y = f . y,z ) )
thus A13: for x being set holds
( x in dom h iff ex y, z being set st
( x = [z,y] & [y,z] in dom f ) ) :: thesis: for y, z being set st [y,z] in dom f holds
h . z,y = f . y,z

proof

let x be set ; :: thesis: ( x in dom h iff ex y, z being set st
( x = [z,y] & [y,z] in dom f ) )
thus ( x in dom h implies ex y, z being set st
( x = [z,y] & [y,z] in dom f ) ) by A3, A11; :: thesis: ( ex y, z being set st
( x = [z,y] & [y,z] in dom f ) implies x in dom h )
given y, z being set such that A14: x = [z,y] and
A15: [y,z] in dom f ; :: thesis: x in dom h
( z in union (union (dom f)) & y in union (union (dom f)) ) by A15, Lm1;
then ( y in D1 & z in D2 ) by A1, A2, A15;
then [z,y] in [:D2,D1:] by ZFMISC_1:106;
hence x in dom h by A3, A11, A14, A15; :: thesis: verum

end;

let y, z be set ; :: thesis: ( [y,z] in dom f implies h . z,y = f . y,z )
assume [y,z] in dom f ; :: thesis: h . z,y = f . y,z
then [z,y] in D by A11, A13;
then consider y', z' being set such that
A16: [z,y] = [z',y'] and
A17: h . z,y = f . [y',z'] by A12;
( z = z' & y = y' ) by A16, ZFMISC_1:33;
hence h . z,y = f . y,z by A17; :: thesis: verum