let f, g be Function; ( f c= g implies ~ f c= ~ g )
assume A1:
f c= g
; ~ f c= ~ g
let x, y be object ; RELAT_1:def 3 ( not [x,y] in ~ f or [x,y] in ~ g )
assume A2:
[x,y] in ~ f
; [x,y] in ~ g
then
x in dom (~ f)
by XTUPLE_0:def 12;
then consider z2, z1 being object such that
A3:
x = [z1,z2]
and
A4:
[z2,z1] in dom f
by FUNCT_4:def 2;
y =
(~ f) . (z1,z2)
by A2, A3, FUNCT_1:1
.=
f . (z2,z1)
by A4, FUNCT_4:def 2
;
then A5:
[[z2,z1],y] in f
by A4, FUNCT_1:1;
then A6:
[z2,z1] in dom g
by A1, FUNCT_1:1;
y = g . (z2,z1)
by A1, A5, FUNCT_1:1;
then A7:
y = (~ g) . (z1,z2)
by A6, FUNCT_4:def 2;
x in dom (~ g)
by A3, A6, FUNCT_4:def 2;
hence
[x,y] in ~ g
by A3, A7, FUNCT_1:1; verum