for X, Y, x, y being set st ( Y is empty implies X is empty ) holds
for F being Function of X,Y
for G being Function of (X \/ {x}),(Y \/ {y}) st G | X = F & G . x = y holds
( ( F is onto implies G is onto ) & ( not y in Y & F is one-to-one implies G is one-to-one ) )