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] )

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

( ( 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

assume
g . x <> f . x
; :: thesis: ex y, z being object st g . x = [y,z]
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]

end;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] )
;

end;

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