let X be set ; :: thesis: for Y being non empty set
for x being object 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 object 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 object ; :: 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 S1[ 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 S1[x,y]
proof
let x9 be Element of [:(Funcs (X,Y)),Y:]; :: thesis: ex y being Element of Funcs ((X \/ {x}),Y) st S1[x9,y]
consider f, y being object 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:66;
Y \/ {y} = Y by A4, ZFMISC_1:40;
then consider F being Function of (X \/ {x}),Y such that
A6: F | X = f and
A7: F . x = y by A1, STIRL2_1:57;
reconsider F9 = F as Element of Funcs ((X \/ {x}),Y) by FUNCT_2:8;
take F9 ; :: thesis: S1[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 :: thesis: for xx being object st xx in X \/ {x} holds
G . xx = F . xx
let xx be object ; :: 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:47, TARSKI:def 1;
hence G . xx = F . xx by A5, A7, A8, A9, XTUPLE_0:1; :: thesis: verum
end;
hence G = F9 by FUNCT_2:12; :: 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 S1[x,H . x] from FUNCT_2:sch 3(A2);
A14: now :: thesis: for x1, x2 being object st x1 in [:(Funcs (X,Y)),Y:] & x2 in [:(Funcs (X,Y)),Y:] & H . x1 = H . x2 holds
x1 = x2
let x1, x2 be object ; :: 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 object 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 object 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:66;
Y \/ {y2} = Y by A19, ZFMISC_1:40;
then consider F2 being Function of (X \/ {x}),Y such that
A24: F2 | X = f2 and
A25: F2 . x = y2 by A1, STIRL2_1:57;
A26: H . x2 = F2 by A13, A16, A20, A24, A25;
Y \/ {y1} = Y by A22, ZFMISC_1:40;
then consider F1 being Function of (X \/ {x}),Y such that
A27: F1 | X = f1 and
A28: F1 . x = y1 by A1, STIRL2_1:57;
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 object ; :: 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:66;
dom f = X \/ {x} by FUNCT_2:def 1;
then A31: dom (f | X) = X by RELAT_1:62, 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:2;
A32: fX in Funcs (X,Y) by FUNCT_2:8;
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 3;
rng f c= Y by RELAT_1:def 19;
then A35: [fX,(f . x)] in [:(Funcs (X,Y)),Y:] by A34, A32, ZFMISC_1:87;
[:(Funcs (X,Y)),Y:] = dom H by FUNCT_2:def 1;
then H . [fX,(f . x)] in rng H by A35, FUNCT_1:def 3;
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;
then ( H is one-to-one & H is onto ) by A14, FUNCT_2:19, 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 3;
A38: f in Funcs (X,Y) by FUNCT_2:8;
rng F c= Y by RELAT_1:def 19;
then [f,(F . x)] in [:(Funcs (X,Y)),Y:] by A37, A38, ZFMISC_1:87;
hence H . (f,(F . x)) = F by A13, A36; :: thesis: verum