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

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