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

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