let f, g be Function; :: thesis: ( dom f is Relation & ~ f c= ~ g implies f c= g )
assume dom f is Relation ; :: thesis: ( not ~ f c= ~ g or f c= g )
then reconsider R = dom f as Relation ;
R c= [:(dom R),(rng R):] by RELAT_1:7;
then A1: ~ (~ f) = f by FUNCT_4:52;
assume ~ f c= ~ g ; :: thesis: f c= g
then ( ~ (~ g) c= g & f c= ~ (~ g) ) by A1, Th44, FUNCT_4:51;
hence f c= g ; :: thesis: verum