let k, n be Nat; for X being non empty set
for A being non empty finite Subset of X
for P being Function of X,(bool X) st ( for x being object st x in X holds
card (P . x) = n ) holds
card { F where F is Element of (k + 1) -tuples_on X : ( F . 1 in A & ( for i being Nat st i in Seg k holds
F . (i + 1) in P . (F . i) ) ) } = (card A) * (n |^ k)
let X be non empty set ; for A being non empty finite Subset of X
for P being Function of X,(bool X) st ( for x being object st x in X holds
card (P . x) = n ) holds
card { F where F is Element of (k + 1) -tuples_on X : ( F . 1 in A & ( for i being Nat st i in Seg k holds
F . (i + 1) in P . (F . i) ) ) } = (card A) * (n |^ k)
let A be non empty finite Subset of X; for P being Function of X,(bool X) st ( for x being object st x in X holds
card (P . x) = n ) holds
card { F where F is Element of (k + 1) -tuples_on X : ( F . 1 in A & ( for i being Nat st i in Seg k holds
F . (i + 1) in P . (F . i) ) ) } = (card A) * (n |^ k)
let P be Function of X,(bool X); ( ( for x being object st x in X holds
card (P . x) = n ) implies card { F where F is Element of (k + 1) -tuples_on X : ( F . 1 in A & ( for i being Nat st i in Seg k holds
F . (i + 1) in P . (F . i) ) ) } = (card A) * (n |^ k) )
assume A1:
for x being object st x in X holds
card (P . x) = n
; card { F where F is Element of (k + 1) -tuples_on X : ( F . 1 in A & ( for i being Nat st i in Seg k holds
F . (i + 1) in P . (F . i) ) ) } = (card A) * (n |^ k)
defpred S1[ Function, Nat] means ( $1 . 1 in A & ( for i being Nat st i in Seg $2 holds
$1 . (i + 1) in P . ($1 . i) ) );
defpred S2[ Nat] means card { F where F is Element of ($1 + 1) -tuples_on X : S1[F,$1] } = (card A) * (n |^ $1);
A2:
dom P = X
by FUNCT_2:def 1;
A3:
for k being Nat st S2[k] holds
S2[k + 1]
proof
let k be
Nat;
( S2[k] implies S2[k + 1] )
set k1 =
k + 1;
set k2 =
(k + 1) + 1;
set F2 =
{ F where F is Element of ((k + 1) + 1) -tuples_on X : S1[F,k + 1] } ;
set F1 =
{ F where F is Element of (k + 1) -tuples_on X : S1[F,k] } ;
defpred S3[
object ,
object ]
means for
f being
FinSequence st $2
= f holds
f | (k + 1) = $1;
assume A4:
S2[
k]
;
S2[k + 1]
then reconsider F1 =
{ F where F is Element of (k + 1) -tuples_on X : S1[F,k] } as
finite set ;
consider PP being
Relation such that A5:
for
x,
y being
object holds
(
[x,y] in PP iff (
x in F1 &
y in { F where F is Element of ((k + 1) + 1) -tuples_on X : S1[F,k + 1] } &
S3[
x,
y] ) )
from RELAT_1:sch 1();
for
x being
object st
x in F1 holds
card (Im (PP,x)) = n
proof
defpred S4[
object ,
object ]
means for
f being
FinSequence st
f = $1 holds
f . ((k + 1) + 1) = $2;
let x be
object ;
( x in F1 implies card (Im (PP,x)) = n )
assume
x in F1
;
card (Im (PP,x)) = n
then consider xx being
Element of
(k + 1) -tuples_on X such that A6:
x = xx
and A7:
S1[
xx,
k]
;
A8:
for
y being
object st
y in Im (
PP,
x) holds
ex
z being
object st
(
z in P . (xx . (k + 1)) &
S4[
y,
z] )
proof
let y be
object ;
( y in Im (PP,x) implies ex z being object st
( z in P . (xx . (k + 1)) & S4[y,z] ) )
assume A9:
y in Im (
PP,
x)
;
ex z being object st
( z in P . (xx . (k + 1)) & S4[y,z] )
A10:
[x,y] in PP
by RELAT_1:169, A9;
then
y in { F where F is Element of ((k + 1) + 1) -tuples_on X : S1[F,k + 1] }
by A5;
then consider yy being
Element of
((k + 1) + 1) -tuples_on X such that A11:
y = yy
and A12:
S1[
yy,
k + 1]
;
take z =
yy . ((k + 1) + 1);
( z in P . (xx . (k + 1)) & S4[y,z] )
A13:
yy . ((k + 1) + 1) in P . (yy . (k + 1))
by FINSEQ_1:3, A12;
yy | (k + 1) = xx
by A11, A10, A5, A6;
hence
(
z in P . (xx . (k + 1)) &
S4[
y,
z] )
by FINSEQ_1:3, FUNCT_1:49, A13, A11;
verum
end;
consider ff being
Function of
(Im (PP,x)),
(P . (xx . (k + 1))) such that A14:
for
z being
object st
z in Im (
PP,
x) holds
S4[
z,
ff . z]
from FUNCT_2:sch 1(A8);
A15:
len xx = k + 1
by CARD_1:def 7;
k + 1
in Seg (k + 1)
by FINSEQ_1:3;
then
k + 1
in dom xx
by A15, FINSEQ_1:def 3;
then A16:
xx . (k + 1) in rng xx
by FUNCT_1:def 3;
then A17:
card (P . (xx . (k + 1))) = n
by A1;
A18:
P . (xx . (k + 1)) in rng P
by A16, A2, FUNCT_1:def 3;
P . (xx . (k + 1)) c= rng ff
proof
let z be
object ;
TARSKI:def 3 ( not z in P . (xx . (k + 1)) or z in rng ff )
assume A19:
z in P . (xx . (k + 1))
;
z in rng ff
reconsider Z =
z as
Element of
X by A18, A19;
set xz =
xx ^ <*Z*>;
A20:
len (xx ^ <*Z*>) = (len xx) + 1
by FINSEQ_2:16;
A21:
(xx ^ <*Z*>) | (k + 1) = xx
by FINSEQ_5:23, A15;
A22:
(
S3[
xx,
xx ^ <*Z*>] &
xx in F1 )
by FINSEQ_5:23, A15, A7;
reconsider xz =
xx ^ <*Z*> as
Element of
((k + 1) + 1) -tuples_on X by A20, A15, FINSEQ_2:92;
A23:
for
i being
Nat st
i in Seg (k + 1) holds
xz . (i + 1) in P . (xz . i)
proof
let i be
Nat;
( i in Seg (k + 1) implies xz . (i + 1) in P . (xz . i) )
assume A24:
i in Seg (k + 1)
;
xz . (i + 1) in P . (xz . i)
then A25:
1
<= i
by FINSEQ_1:1;
A26:
i <= k + 1
by A24, FINSEQ_1:1;
per cases
( i <= k or i = k + 1 )
by A26, NAT_1:8;
suppose A27:
i <= k
;
xz . (i + 1) in P . (xz . i)
1
<= 1
+ i
by NAT_1:11;
then
i + 1
in dom xx
by A27, XREAL_1:6, A15, FINSEQ_3:25;
then A28:
xz . (i + 1) = xx . (i + 1)
by FINSEQ_1:def 7;
i < k + 1
by A27, NAT_1:13;
then A29:
i in dom xx
by A25, A15, FINSEQ_3:25;
xx . (i + 1) in P . (xx . i)
by A27, A25, FINSEQ_1:1, A7;
hence
xz . (i + 1) in P . (xz . i)
by A28, A29, FINSEQ_1:def 7;
verum
end;
1
<= k + 1
by NAT_1:11;
then
1
in dom xx
by FINSEQ_3:25, A15;
then
xz . 1
= xx . 1
by FINSEQ_1:def 7;
then
xz in { F where F is Element of ((k + 1) + 1) -tuples_on X : S1[F,k + 1] }
by A23, A7;
then A31:
[xx,xz] in PP
by A5, A22;
then A32:
xz in Im (
PP,
xx)
by RELAT_1:169;
ex
d being
object st
(
d in P . (xx . (k + 1)) &
S4[
xz,
d] )
by A31, RELAT_1:169, A6, A8;
then A33:
dom ff = Im (
PP,
xx)
by FUNCT_2:def 1, A6;
ff . xz =
xz . ((k + 1) + 1)
by A31, RELAT_1:169, A14, A6
.=
z
by FINSEQ_1:42, A15
;
hence
z in rng ff
by A33, A32, FUNCT_1:def 3;
verum
end;
then A34:
P . (xx . (k + 1)) = rng ff
;
per cases
( P . (xx . (k + 1)) is empty or not P . (xx . (k + 1)) is empty )
;
suppose A37:
not
P . (xx . (k + 1)) is
empty
;
card (Im (PP,x)) = nA38:
ff is
one-to-one
proof
let x1,
x2 be
object ;
FUNCT_1:def 4 ( not x1 in dom ff or not x2 in dom ff or not ff . x1 = ff . x2 or x1 = x2 )
assume that A39:
x1 in dom ff
and A40:
x2 in dom ff
and A41:
ff . x1 = ff . x2
;
x1 = x2
A42:
[xx,x1] in PP
by A39, RELAT_1:169, A6;
then
x1 in { F where F is Element of ((k + 1) + 1) -tuples_on X : S1[F,k + 1] }
by A5;
then consider f1 being
Element of
((k + 1) + 1) -tuples_on X such that A43:
x1 = f1
and
S1[
f1,
k + 1]
;
A44:
len f1 = (k + 1) + 1
by CARD_1:def 7;
f1 | (k + 1) = xx
by A42, A43, A5;
then A45:
f1 = xx ^ <*(f1 . ((k + 1) + 1))*>
by A44, FINSEQ_3:55;
A46:
[xx,x2] in PP
by A40, RELAT_1:169, A6;
then
x2 in { F where F is Element of ((k + 1) + 1) -tuples_on X : S1[F,k + 1] }
by A5;
then consider f2 being
Element of
((k + 1) + 1) -tuples_on X such that A47:
x2 = f2
and
S1[
f2,
k + 1]
;
A48:
len f2 = (k + 1) + 1
by CARD_1:def 7;
f2 | (k + 1) = xx
by A46, A47, A5;
then A49:
f2 = xx ^ <*(f2 . ((k + 1) + 1))*>
by A48, FINSEQ_3:55;
f1 . ((k + 1) + 1) = ff . x1
by A39, A14, A43;
hence
x1 = x2
by A45, A49, A40, A14, A47, A41, A43;
verum
end;
dom ff = Im (
PP,
x)
by A37, FUNCT_2:def 1;
hence
card (Im (PP,x)) = n
by A38, A34, WELLORD2:def 4, CARD_1:5, A17;
verum end;
end;
then A50:
card PP = (card (PP | ((dom PP) \ F1))) +` (n *` (card F1))
by SIMPLEX1:1;
dom PP c= F1
then
(dom PP) \ F1 = {}
by XBOOLE_1:37;
then
card (PP | ((dom PP) \ F1)) = 0
;
then
card PP = n *` (card F1)
by A50, CARD_2:18;
then A51:
card PP =
n * (card F1)
by Lm1
.=
(card A) * (n * (n |^ k))
by A4
.=
(card A) * (n |^ (k + 1))
by NEWTON:6
;
A52:
for
f2 being
Element of
((k + 1) + 1) -tuples_on X st
S1[
f2,
k + 1] holds
[(f2 | (k + 1)),f2] in PP
proof
let f2 be
Element of
((k + 1) + 1) -tuples_on X;
( S1[f2,k + 1] implies [(f2 | (k + 1)),f2] in PP )
assume A53:
S1[
f2,
k + 1]
;
[(f2 | (k + 1)),f2] in PP
A54:
f2 in { F where F is Element of ((k + 1) + 1) -tuples_on X : S1[F,k + 1] }
by A53;
set f1 =
f2 | (k + 1);
A55:
S3[
f2 | (k + 1),
f2]
;
(
len f2 = (k + 1) + 1 &
k + 1
< (k + 1) + 1 )
by CARD_1:def 7, NAT_1:13;
then
len (f2 | (k + 1)) = k + 1
by FINSEQ_1:59;
then reconsider f1 =
f2 | (k + 1) as
Element of
(k + 1) -tuples_on X by FINSEQ_2:92;
A56:
for
i being
Nat st
i in Seg k holds
f1 . (i + 1) in P . (f1 . i)
1
<= k + 1
by NAT_1:11;
then
1
in Seg (k + 1)
;
then
S1[
f1,
k]
by A56, FUNCT_1:49, A53;
then
f1 in F1
;
hence
[(f2 | (k + 1)),f2] in PP
by A54, A55, A5;
verum
end;
per cases
( n = 0 or n > 0 )
;
suppose A64:
n > 0
;
S2[k + 1]defpred S4[
object ,
object ]
means for
x,
y being
object st $1
= [x,y] holds
$2
= y;
A65:
for
y being
object st
y in PP holds
ex
z being
object st
(
z in { F where F is Element of ((k + 1) + 1) -tuples_on X : S1[F,k + 1] } &
S4[
y,
z] )
proof
let y be
object ;
( y in PP implies ex z being object st
( z in { F where F is Element of ((k + 1) + 1) -tuples_on X : S1[F,k + 1] } & S4[y,z] ) )
assume A66:
y in PP
;
ex z being object st
( z in { F where F is Element of ((k + 1) + 1) -tuples_on X : S1[F,k + 1] } & S4[y,z] )
then consider y1,
y2 being
object such that A67:
y = [y1,y2]
by RELAT_1:def 1;
take
y2
;
( y2 in { F where F is Element of ((k + 1) + 1) -tuples_on X : S1[F,k + 1] } & S4[y,y2] )
thus
(
y2 in { F where F is Element of ((k + 1) + 1) -tuples_on X : S1[F,k + 1] } &
S4[
y,
y2] )
by XTUPLE_0:1, A66, A67, A5;
verum
end; consider pr being
Function of
PP,
{ F where F is Element of ((k + 1) + 1) -tuples_on X : S1[F,k + 1] } such that A68:
for
y being
object st
y in PP holds
S4[
y,
pr . y]
from FUNCT_2:sch 1(A65);
A69:
pr is
one-to-one
proof
let x1,
x2 be
object ;
FUNCT_1:def 4 ( not x1 in dom pr or not x2 in dom pr or not pr . x1 = pr . x2 or x1 = x2 )
assume that A70:
x1 in dom pr
and A71:
x2 in dom pr
and A72:
pr . x1 = pr . x2
;
x1 = x2
consider y1,
z1 being
object such that A73:
x1 = [y1,z1]
by A70, RELAT_1:def 1;
A74:
pr . x1 = z1
by A68, A70, A73;
consider y2,
z2 being
object such that A75:
x2 = [y2,z2]
by A71, RELAT_1:def 1;
A76:
pr . x2 = z2
by A68, A71, A75;
z1 in { F where F is Element of ((k + 1) + 1) -tuples_on X : S1[F,k + 1] }
by A73, A70, A5;
then consider f1 being
Element of
((k + 1) + 1) -tuples_on X such that A77:
z1 = f1
and
S1[
f1,
k + 1]
;
f1 | (k + 1) = y1
by A73, A70, A5, A77;
hence
x1 = x2
by A71, A5, A75, A72, A73, A74, A76, A77;
verum
end;
not
{ F where F is Element of ((k + 1) + 1) -tuples_on X : S1[F,k + 1] } is
empty
then A79:
dom pr = PP
by FUNCT_2:def 1;
{ F where F is Element of ((k + 1) + 1) -tuples_on X : S1[F,k + 1] } c= rng pr
then
{ F where F is Element of ((k + 1) + 1) -tuples_on X : S1[F,k + 1] } = rng pr
;
hence
S2[
k + 1]
by A69, A79, WELLORD2:def 4, A51, CARD_1:5;
verum end;
end;
A82:
S2[ 0 ]
proof
deffunc H1(
object )
-> set =
<*$1*>;
set F0 =
{ F where F is Element of (0 + 1) -tuples_on X : S1[F, 0 ] } ;
A83:
for
x being
object st
x in A holds
H1(
x)
in { F where F is Element of (0 + 1) -tuples_on X : S1[F, 0 ] }
consider f being
Function of
A,
{ F where F is Element of (0 + 1) -tuples_on X : S1[F, 0 ] } such that A86:
for
x being
object st
x in A holds
f . x = H1(
x)
from FUNCT_2:sch 2(A83);
H1( the
Element of
A)
in { F where F is Element of (0 + 1) -tuples_on X : S1[F, 0 ] }
by A83;
then A87:
dom f = A
by FUNCT_2:def 1;
{ F where F is Element of (0 + 1) -tuples_on X : S1[F, 0 ] } c= rng f
then A91:
rng f = { F where F is Element of (0 + 1) -tuples_on X : S1[F, 0 ] }
;
A92:
f is
one-to-one
n |^ 0 = 1
by NEWTON:4;
hence
S2[
0 ]
by A91, WELLORD2:def 4, A87, A92, CARD_1:5;
verum
end;
for k being Nat holds S2[k]
from NAT_1:sch 2(A82, A3);
hence
card { F where F is Element of (k + 1) -tuples_on X : ( F . 1 in A & ( for i being Nat st i in Seg k holds
F . (i + 1) in P . (F . i) ) ) } = (card A) * (n |^ k)
; verum