let X, Y be set ; :: thesis: 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 )
let x, y be object ; :: thesis: ( ( Y is empty implies X is empty ) & not x in X implies for F being Function of X,Y ex G being Function of (X \/ {x}),(Y \/ {y}) st
( G | X = F & G . x = y ) )
assume that
A1: ( Y is empty implies X is empty ) and
A2: not x in X ; :: thesis: for F being Function of X,Y ex G being Function of (X \/ {x}),(Y \/ {y}) st
( G | X = F & G . x = y )
set Y1 = Y \/ {y};
set X1 = X \/ {x};
deffunc H₁( set ) -> object = y;
let F be Function of X,Y; :: thesis: ex G being Function of (X \/ {x}),(Y \/ {y}) st
( G | X = F & G . x = y )
y in {y} by TARSKI:def 1;
then A3: for x9 being set st x9 in (X \/ {x}) \ X holds
H₁(x9) in Y \/ {y} by XBOOLE_0:def 3;
A4: ( X c= X \/ {x} & Y c= Y \/ {y} ) by XBOOLE_1:7;
consider G being Function of (X \/ {x}),(Y \/ {y}) such that
A5: ( G | X = F & ( for x9 being set st x9 in (X \/ {x}) \ X holds
G . x9 = H₁(x9) ) ) from STIRL2_1:sch 2(A3, A4, A1);
x in {x} by TARSKI:def 1;
then x in X \/ {x} by XBOOLE_0:def 3;
then x in (X \/ {x}) \ X by A2, XBOOLE_0:def 5;
then G . x = y by A5;
hence ex G being Function of (X \/ {x}),(Y \/ {y}) st
( G | X = F & G . x = y ) by A5; :: thesis: verum