let X be set ; 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 ; 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 ; ( 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
; 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:];
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
;
S1[x9,F9]
let g be
Function of
X,
Y;
for F being Function of (X \/ {x}),Y
for y being set st [g,y] = x9 & F . x = y & F | X = g holds
F = F9let G be
Function of
(X \/ {x}),
Y;
for y being set st [g,y] = x9 & G . x = y & G | X = g holds
G = F9let y9 be
set ;
( [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
;
G = F9
hence
G = F9
by FUNCT_2:12;
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 for x1, x2 being object st x1 in [:(Funcs (X,Y)),Y:] & x2 in [:(Funcs (X,Y)),Y:] & H . x1 = H . x2 holds
x1 = x2let x1,
x2 be
object ;
( 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
;
x1 = x2consider 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;
verum end;
take
H
; ( 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 ;
TARSKI:def 3 ( not f9 in Funcs ((X \/ {x}),Y) or f9 in rng H )
assume
f9 in Funcs (
(X \/ {x}),
Y)
;
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;
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
; 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; 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; ( F | X = f implies H . (f,(F . x)) = F )
assume A36:
F | X = f
; 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; verum