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 by A1, TARSKI:def 3;
then A3: (Y --> b) . x = b by FUNCOP_1:13;
( dom (X --> a) = X & (X --> a) . x = a ) by A1, FUNCOP_1:13, FUNCOP_1:19;
hence a = b by A1, A2, A3, GRFUNC_1:8; :: thesis: verum