let f, g be Function; :: thesis: ( f c= g implies ~ f c= ~ g )
assume A1: f c= g ; :: thesis: ~ f c= ~ g
let x be set ; :: according to RELAT_1:def 3 :: thesis: for b₁ being set holds
( not [x,b₁] in ~ f or [x,b₁] in ~ g )
let y be set ; :: 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 RELAT_1:def 4;
then consider z2, z1 being set 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:8
.= f . z2,z1 by A4, FUNCT_4:def 2 ;
then A5: [[z2,z1],y] in f by A4, FUNCT_1:8;
then A6: [z2,z1] in dom g by A1, FUNCT_1:8;
y = g . z2,z1 by A1, A5, FUNCT_1:8;
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:8; :: thesis: verum