let f, g be Function; :: thesis: ( f c= g implies ~ f c= ~ g )
assume A1: f c= g ; :: thesis: ~ f c= ~ g
let x, y be object ; :: according to RELAT_1:def 3 :: thesis: ( not [x,y] in ~ f or [x,y] in ~ g )
assume A2: [x,y] in ~ f ; :: thesis: [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; :: thesis: verum