let X, Y be set ; :: thesis: for a, b being object st X <> {} & X --> a c= Y --> b holds
a = b
let a, b be object ; :: thesis: ( X <> {} & X --> a c= Y --> b implies a = b )
assume A1: X <> {} ; :: thesis: ( not X --> a c= Y --> b or a = b )
set x = the Element of X;
assume A2: X --> a c= Y --> b ; :: thesis: a = b
then X c= Y by Th5;
then the Element of X in Y by A1;
then A3: (Y --> b) . the Element of X = b by FUNCOP_1:7;
( dom (X --> a) = X & (X --> a) . the Element of X = a ) by A1, FUNCOP_1:7;
hence a = b by A1, A2, A3, GRFUNC_1:2; :: thesis: verum