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

proof

let x, y1, y2 be object ; :: 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 object such that A5: x = [z,y] and
A6: y1 = f . [y,z] ; :: thesis: ( not S₁[x,y2] or y1 = y2 )
given y9, z9 being object such that A7: x = [z9,y9] and
A8: y2 = f . [y9,z9] ; :: thesis: y1 = y2
z = z9 by A5, A7, XTUPLE_0:1;
hence y1 = y2 by A5, A6, A7, A8, XTUPLE_0:1; :: thesis: verum

end;

A9: for x being object st x in D holds
ex y1 being object st S₁[x,y1]

proof

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

end;

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

proof

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

end;

let y, z be object ; :: 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 y9, z9 being object such that
A17: [z,y] = [z9,y9] and
A18: h . (z,y) = f . [y9,z9] by A12;
z = z9 by A17, XTUPLE_0:1;
hence h . (z,y) = f . (y,z) by A17, A18, XTUPLE_0:1; :: thesis: verum