let g, f be Function; :: thesis: ( dom g = dom f & ( for x being object st x in dom f holds
( ( for y, z being object st f . x = [y,z] holds
g . x = [z,y] ) & ( f . x = g . x or ex y, z being object st f . x = [y,z] ) ) ) implies ( dom f = dom g & ( for x being object st x in dom g holds
( ( for y, z being object st g . x = [y,z] holds
f . x = [z,y] ) & ( g . x = f . x or ex y, z being object st g . x = [y,z] ) ) ) ) )
assume that
A17: dom g = dom f and
A18: for x being object st x in dom f holds
( ( for y, z being object st f . x = [y,z] holds
g . x = [z,y] ) & ( f . x = g . x or ex y, z being object st f . x = [y,z] ) ) ; :: thesis: ( dom f = dom g & ( for x being object st x in dom g holds
( ( for y, z being object st g . x = [y,z] holds
f . x = [z,y] ) & ( g . x = f . x or ex y, z being object st g . x = [y,z] ) ) ) )
thus dom f = dom g by A17; :: thesis: for x being object st x in dom g holds
( ( for y, z being object st g . x = [y,z] holds
f . x = [z,y] ) & ( g . x = f . x or ex y, z being object st g . x = [y,z] ) )
let x be object ; :: thesis: ( x in dom g implies ( ( for y, z being object st g . x = [y,z] holds
f . x = [z,y] ) & ( g . x = f . x or ex y, z being object st g . x = [y,z] ) ) )
assume A19: x in dom g ; :: thesis: ( ( for y, z being object st g . x = [y,z] holds
f . x = [z,y] ) & ( g . x = f . x or ex y, z being object st g . x = [y,z] ) )
thus for y, z being object st g . x = [y,z] holds
f . x = [z,y] :: thesis: ( g . x = f . x or ex y, z being object st g . x = [y,z] )

proof

let y, z be object ; :: thesis: ( g . x = [y,z] implies f . x = [z,y] )
assume A20: g . x = [y,z] ; :: thesis: f . x = [z,y]

per cases ( ex z, y being object st f . x = [z,y] or for z, y being object holds not f . x = [z,y] ) ;

suppose ex z, y being object st f . x = [z,y] ; :: thesis: f . x = [z,y]

then consider y1, y2 being object such that
A21: f . x = [y1,y2] ;
A22: g . x = [y2,y1] by A17, A18, A19, A21;
then y = y2 by A20, XTUPLE_0:1;
hence f . x = [z,y] by A20, A21, A22, XTUPLE_0:1; :: thesis: verum

end;

suppose for z, y being object holds not f . x = [z,y] ; :: thesis: f . x = [z,y]

then f . x = g . x by A17, A18, A19;
hence f . x = [z,y] by A17, A18, A19, A20; :: thesis: verum

end;

end;

end;

assume g . x <> f . x ; :: thesis: ex y, z being object st g . x = [y,z]
then consider y, z being object such that
A23: f . x = [y,z] by A17, A18, A19;
take z ; :: thesis: ex z being object st g . x = [z,z]
take y ; :: thesis: g . x = [z,y]
thus g . x = [z,y] by A17, A18, A19, A23; :: thesis: verum