theorem Th57: :: STIRL2_1:57

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