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 ( dom (X --> a) c= dom (Y --> b) & dom (X --> a) = X & dom (Y --> b) = Y ) by FUNCOP_1:19, RELAT_1:25;
hence X c= Y ; :: thesis: verum