let X be set ; :: thesis: for Y being non empty set
for x being set st not x in X holds
ex BIJECT being Function of [:(Funcs X,Y),Y:],(Funcs (X \/ {x}),Y) st
( BIJECT is bijective & ( for f being Function of X,Y
for F being Function of (X \/ {x}),Y st F | X = f holds
BIJECT . f,(F . x) = F ) )
let Y be non empty set ; :: thesis: for x being set st not x in X holds
ex BIJECT being Function of [:(Funcs X,Y),Y:],(Funcs (X \/ {x}),Y) st
( BIJECT is bijective & ( for f being Function of X,Y
for F being Function of (X \/ {x}),Y st F | X = f holds
BIJECT . f,(F . x) = F ) )
let x be set ; :: thesis: ( not x in X implies ex BIJECT being Function of [:(Funcs X,Y),Y:],(Funcs (X \/ {x}),Y) st
( BIJECT is bijective & ( for f being Function of X,Y
for F being Function of (X \/ {x}),Y st F | X = f holds
BIJECT . f,(F . x) = F ) ) )
assume A1: not x in X ; :: thesis: ex BIJECT being Function of [:(Funcs X,Y),Y:],(Funcs (X \/ {x}),Y) st
( BIJECT is bijective & ( for f being Function of X,Y
for F being Function of (X \/ {x}),Y st F | X = f holds
BIJECT . f,(F . x) = F ) )
set Xx = X \/ {x};
set FXY = Funcs X,Y;
set FXxY = Funcs (X \/ {x}),Y;
defpred S₁[ set , set ] means for f being Function of X,Y
for F being Function of (X \/ {x}),Y
for y being set st [f,y] = $1 & F . x = y & F | X = f holds
F = $2;
A2: for x being Element of [:(Funcs X,Y),Y:] ex y being Element of Funcs (X \/ {x}),Y st S₁[x,y]

proof

let x9 be Element of [:(Funcs X,Y),Y:]; :: thesis: ex y being Element of Funcs (X \/ {x}),Y st S₁[x9,y]
consider f, y being set such that
A3: f in Funcs X,Y and
A4: y in Y and
A5: x9 = [f,y] by ZFMISC_1:def 2;
reconsider f = f as Function of X,Y by A3, FUNCT_2:121;
Y \/ {y} = Y by A4, ZFMISC_1:46;
then consider F being Function of (X \/ {x}),Y such that
A6: F | X = f and
A7: F . x = y by A1, STIRL2_1:67;
reconsider F9 = F as Element of Funcs (X \/ {x}),Y by FUNCT_2:11;
take F9 ; :: thesis: S₁[x9,F9]
let g be Function of X,Y; :: thesis: for F being Function of (X \/ {x}),Y
for y being set st [g,y] = x9 & F . x = y & F | X = g holds
F = F9
let G be Function of (X \/ {x}),Y; :: thesis: for y being set st [g,y] = x9 & G . x = y & G | X = g holds
G = F9
let y9 be set ; :: thesis: ( [g,y9] = x9 & G . x = y9 & G | X = g implies G = F9 )
assume that
A8: [g,y9] = x9 and
A9: G . x = y9 and
A10: G | X = g ; :: thesis: G = F9

now

let xx be set ; :: thesis: ( xx in X \/ {x} implies G . xx = F . xx )
assume xx in X \/ {x} ; :: thesis: G . xx = F . xx
then A11: ( xx in X or xx in {x} ) by XBOOLE_0:def 3;
A12: dom f = X by FUNCT_2:def 1;
dom g = X by FUNCT_2:def 1;
then ( ( G . xx = g . xx & F . xx = f . xx ) or xx = x ) by A6, A10, A11, A12, FUNCT_1:70, TARSKI:def 1;
hence G . xx = F . xx by A5, A7, A8, A9, ZFMISC_1:33; :: thesis: verum

end;

hence G = F9 by FUNCT_2:18; :: thesis: verum

end;

consider H being Function of [:(Funcs X,Y),Y:],(Funcs (X \/ {x}),Y) such that
A13: for x being Element of [:(Funcs X,Y),Y:] holds S₁[x,H . x] from FUNCT_2:sch 3(A2);

A14: now

let x1, x2 be set ; :: thesis: ( x1 in [:(Funcs X,Y),Y:] & x2 in [:(Funcs X,Y),Y:] & H . x1 = H . x2 implies x1 = x2 )
assume that
A15: x1 in [:(Funcs X,Y),Y:] and
A16: x2 in [:(Funcs X,Y),Y:] and
A17: H . x1 = H . x2 ; :: thesis: x1 = x2
consider f2, y2 being set such that
A18: f2 in Funcs X,Y and
A19: y2 in Y and
A20: x2 = [f2,y2] by A16, ZFMISC_1:def 2;
consider f1, y1 being set such that
A21: f1 in Funcs X,Y and
A22: y1 in Y and
A23: x1 = [f1,y1] by A15, ZFMISC_1:def 2;
reconsider f1 = f1, f2 = f2 as Function of X,Y by A21, A18, FUNCT_2:121;
Y \/ {y2} = Y by A19, ZFMISC_1:46;
then consider F2 being Function of (X \/ {x}),Y such that
A24: F2 | X = f2 and
A25: F2 . x = y2 by A1, STIRL2_1:67;
A26: H . x2 = F2 by A13, A16, A20, A24, A25;
Y \/ {y1} = Y by A22, ZFMISC_1:46;
then consider F1 being Function of (X \/ {x}),Y such that
A27: F1 | X = f1 and
A28: F1 . x = y1 by A1, STIRL2_1:67;
H . x1 = F1 by A13, A15, A23, A27, A28;
hence x1 = x2 by A17, A23, A20, A27, A28, A24, A25, A26; :: thesis: verum

end;

take H ; :: thesis: ( H is bijective & ( for f being Function of X,Y
for F being Function of (X \/ {x}),Y st F | X = f holds
H . f,(F . x) = F ) )
x in {x} by TARSKI:def 1;
then A29: x in X \/ {x} by XBOOLE_0:def 3;
A30: Funcs (X \/ {x}),Y c= rng H

proof

let f9 be set ; :: according to TARSKI:def 3 :: thesis: ( not f9 in Funcs (X \/ {x}),Y or f9 in rng H )
assume f9 in Funcs (X \/ {x}),Y ; :: thesis: f9 in rng H
then reconsider f = f9 as Function of (X \/ {x}),Y by FUNCT_2:121;
dom f = X \/ {x} by FUNCT_2:def 1;
then A31: dom (f | X) = X by RELAT_1:91, XBOOLE_1:7;
rng (f | X) c= Y by RELAT_1:def 19;
then reconsider fX = f | X as Function of X,Y by A31, FUNCT_2:4;
A32: fX in Funcs X,Y by FUNCT_2:11;
x in {x} by TARSKI:def 1;
then A33: x in X \/ {x} by XBOOLE_0:def 3;
X \/ {x} = dom f by FUNCT_2:def 1;
then A34: f . x in rng f by A33, FUNCT_1:def 5;
rng f c= Y by RELAT_1:def 19;
then A35: [fX,(f . x)] in [:(Funcs X,Y),Y:] by A34, A32, ZFMISC_1:106;
[:(Funcs X,Y),Y:] = dom H by FUNCT_2:def 1;
then H . [fX,(f . x)] in rng H by A35, FUNCT_1:def 5;
hence f9 in rng H by A13, A35; :: thesis: verum

end;

rng H c= Funcs (X \/ {x}),Y by RELAT_1:def 19;
then Funcs (X \/ {x}),Y = rng H by A30, XBOOLE_0:def 10;
then ( H is one-to-one & H is onto ) by A14, FUNCT_2:25, FUNCT_2:def 3;
hence H is bijective ; :: thesis: for f being Function of X,Y
for F being Function of (X \/ {x}),Y st F | X = f holds
H . f,(F . x) = F
let f be Function of X,Y; :: thesis: for F being Function of (X \/ {x}),Y st F | X = f holds
H . f,(F . x) = F
let F be Function of (X \/ {x}),Y; :: thesis: ( F | X = f implies H . f,(F . x) = F )
assume A36: F | X = f ; :: thesis: H . f,(F . x) = F
X \/ {x} = dom F by FUNCT_2:def 1;
then A37: F . x in rng F by A29, FUNCT_1:def 5;
A38: f in Funcs X,Y by FUNCT_2:11;
rng F c= Y by RELAT_1:def 19;
then [f,(F . x)] in [:(Funcs X,Y),Y:] by A37, A38, ZFMISC_1:106;
hence H . f,(F . x) = F by A13, A36; :: thesis: verum