theorem :: FUNCT_4:6

for X, Y being set
for a, b being object st X <> {} & X --> a c= Y --> b holds
a = b