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_{1}( 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_{1}(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_{1}(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

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

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

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

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