let h1, h2 be Function; :: thesis: ( ( for x being object holds
( x in dom h1 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
h1 . (z,y) = f . (y,z) ) & ( for x being object holds
( x in dom h2 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
h2 . (z,y) = f . (y,z) ) implies h1 = h2 )
assume that
A19: for x being object holds
( x in dom h1 iff ex y, z being object st
( x = [z,y] & [y,z] in dom f ) ) and
A20: for y, z being object st [y,z] in dom f holds
h1 . (z,y) = f . (y,z) and
A21: for x being object holds
( x in dom h2 iff ex y, z being object st
( x = [z,y] & [y,z] in dom f ) ) and
A22: for y, z being object st [y,z] in dom f holds
h2 . (z,y) = f . (y,z) ; :: thesis: h1 = h2
A23: for x being object st x in dom h1 holds
h1 . x = h2 . x

proof

let x be object ; :: thesis: ( x in dom h1 implies h1 . x = h2 . x )
assume x in dom h1 ; :: thesis: h1 . x = h2 . x
then consider x1, x2 being object such that
A24: x = [x2,x1] and
A25: [x1,x2] in dom f by A19;
h1 . (x2,x1) = f . (x1,x2) by A20, A25
.= h2 . (x2,x1) by A22, A25 ;
hence h1 . x = h2 . x by A24; :: thesis: verum

end;

for x being object holds
( x in dom h1 iff x in dom h2 )

proof

let x be object ; :: thesis: ( x in dom h1 iff x in dom h2 )
( x in dom h1 iff ex y, z being object st
( x = [z,y] & [y,z] in dom f ) ) by A19;
hence ( x in dom h1 iff x in dom h2 ) by A21; :: thesis: verum

end;

then dom h1 = dom h2 by TARSKI:2;
hence h1 = h2 by A23; :: thesis: verum