let X, Y be set ; :: thesis: for a, b being object st X --> a c= Y --> b holds
X c= Y
let a, b be object ; :: 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;
thus X c= Y by A1; :: thesis: verum