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:21;
then A1: ( ~ (~ f) = f & ~ (~ g) c= g ) by FUNCT_4:52, FUNCT_4:53;
assume ~ f c= ~ g ; :: thesis: f c= g
then f c= ~ (~ g) by A1, Th45;
hence f c= g by A1, XBOOLE_1:1; :: thesis: verum