let X, a, Y, b be set ; :: thesis: ( X <> {} & X --> a c= Y --> b implies a = b )
assume A1: X <> {} ; :: thesis: ( not X --> a c= Y --> b or a = b )
consider x being Element of X;
assume A2: X --> a c= Y --> b ; :: thesis: a = b
then X c= Y by Th6;
then ( x in Y & dom (X --> a) = X ) by A1, FUNCOP_1:19, TARSKI:def 3;
then ( (X --> a) . x = a & (Y --> b) . x = b & (X --> a) . x = (Y --> b) . x ) by A1, A2, FUNCOP_1:13, GRFUNC_1:8;
hence a = b ; :: thesis: verum