let X, Y, x, y be set ; :: 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 )
let F be Function of X,Y; :: thesis: ex G being Function of (X \/ {x}),(Y \/ {y}) st
( G | X = F & G . x = y )
deffunc H₁( set ) -> set = y;
set X1 = X \/ {x};
set Y1 = Y \/ {y};
A3: ( X c= X \/ {x} & Y c= Y \/ {y} ) by XBOOLE_1:7;
A4: for x' being set st x' in (X \/ {x}) \ X holds
H₁(x') in Y \/ {y}

proof

y in {y} by TARSKI:def 1;
hence for x' being set st x' in (X \/ {x}) \ X holds
H₁(x') in Y \/ {y} by XBOOLE_0:def 3; :: thesis: verum

end;

consider G being Function of (X \/ {x}),(Y \/ {y}) such that
A5: ( G | X = F & ( for x' being set st x' in (X \/ {x}) \ X holds
G . x' = H₁(x') ) ) from STIRL2_1:sch 2(A4, A3, 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