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] & [z2,z1] in dom f ) by FUNCT_4:def 2;
y = (~ f) . z1,z2 by A2, A3, FUNCT_1:8
.= f . z2,z1 by A3, FUNCT_4:def 2 ;
then [[z2,z1],y] in f by A3, FUNCT_1:8;
then ( [z2,z1] in dom g & y = g . z2,z1 ) by A1, FUNCT_1:8;
then ( x in dom (~ g) & y = (~ g) . z1,z2 ) by A3, FUNCT_4:def 2;
hence [x,y] in ~ g by A3, FUNCT_1:8; :: thesis: verum