let X, a, Y, b be set ; :: thesis: ( X --> a c= Y --> b implies X c= Y )
assume X --> a c= Y --> b ; :: thesis: X c= Y
then A1: dom (X --> a) c= dom (Y --> b) by RELAT_1:11;
dom (X --> a) = X by FUNCOP_1:13;
hence X c= Y by A1, FUNCOP_1:13; :: thesis: verum