let k, n be Nat; :: thesis:
let X be non empty set ; :: thesis:
let A be non empty finite Subset of X; :: thesis:
let P be Function of X,(bool X); :: thesis:
assume A1: for x being object st x in X holds
card (P . x) = n ; :: thesis:
defpred S₁[ 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 S₂[ Nat] means card { F where F is Element of ($1 + 1) -tuples_on X : S₁[F,$1] } = (card A) * (n |^ $1);
A2: dom P = X by FUNCT_2:def 1;
A3: for k being Nat st S₂[k] holds
S₂[k + 1]

let k be Nat; :: thesis:
set k1 = k + 1;
set k2 = (k + 1) + 1;
set F2 = { F where F is Element of ((k + 1) + 1) -tuples_on X : S₁[F,k + 1] } ;
set F1 = { F where F is Element of (k + 1) -tuples_on X : S₁[F,k] } ;
defpred S₃[ object , object ] means for f being FinSequence st $2 = f holds
f | (k + 1) = $1;
assume A4: S₂[k] ; :: thesis:
then reconsider F1 = { F where F is Element of (k + 1) -tuples_on X : S₁[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 : S₁[F,k + 1] } & S₃[x,y] ) ) from RELAT_1:sch 1();
for x being object st x in F1 holds
card (Im (PP,x)) = n

defpred S₄[ object , object ] means for f being FinSequence st f = $1 holds
f . ((k + 1) + 1) = $2;
let x be object ; :: thesis:
assume x in F1 ; :: thesis:
then consider xx being Element of (k + 1) -tuples_on X such that
A6: x = xx and
A7: S₁[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)) & S₄[y,z] )

proof

let y be object ; :: thesis:
assume A9: y in Im (PP,x) ; :: thesis:
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 : S₁[F,k + 1] } by A5;
then consider yy being Element of ((k + 1) + 1) -tuples_on X such that
A11: y = yy and
A12: S₁[yy,k + 1] ;
take z = yy . ((k + 1) + 1); :: thesis:
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)) & S₄[y,z] ) by FINSEQ_1:3, FUNCT_1:49, A13, A11; :: thesis:

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
S₄[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 ; :: according to TARSKI:def 3 :: thesis:
assume A19: z in P . (xx . (k + 1)) ; :: thesis:
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: ( S₃[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; :: thesis:
assume A24: i in Seg (k + 1) ; :: thesis:
then A25: 1 <= i by FINSEQ_1:1;
A26: i <= k + 1 by A24, FINSEQ_1:1;

per cases by A26, NAT_1:8;

suppose A27: i <= k ; :: thesis:

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; :: thesis:

end;

suppose A30: i = k + 1 ; :: thesis:

then xz . i = xx . i by A21, FINSEQ_1:3, FUNCT_1:49;
hence xz . (i + 1) in P . (xz . i) by A30, FINSEQ_1:42, A15, A19; :: thesis:

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 : S₁[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)) & S₄[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; :: thesis:

end;

then A34: P . (xx . (k + 1)) = rng ff ;

per cases ;

suppose A35: P . (xx . (k + 1)) is empty ; :: thesis:

Im (PP,x) is empty

proof

assume not Im (PP,x) is empty ; :: thesis:
then consider d being object such that
A36: d in Im (PP,x) ;
ex z being object st
( z in P . (xx . (k + 1)) & S₄[d,z] ) by A36, A8;
hence contradiction by A35; :: thesis:

end;

hence card (Im (PP,x)) = n by A35, A16, A1; :: thesis:

end;

suppose A37: not P . (xx . (k + 1)) is empty ; :: thesis:

A38: ff is one-to-one

proof

let x1, x2 be object ; :: according to FUNCT_1:def 4 :: thesis:
assume that
A39: x1 in dom ff and
A40: x2 in dom ff and
A41: ff . x1 = ff . x2 ; :: thesis:
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 : S₁[F,k + 1] } by A5;
then consider f1 being Element of ((k + 1) + 1) -tuples_on X such that
A43: x1 = f1 and
S₁[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 : S₁[F,k + 1] } by A5;
then consider f2 being Element of ((k + 1) + 1) -tuples_on X such that
A47: x2 = f2 and
S₁[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; :: thesis:

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; :: thesis:

end;

then A50: card PP = (card (PP | ((dom PP) \ F1))) +` (n *` (card F1)) by SIMPLEX1:1;
dom PP c= F1

proof

let y be object ; :: according to TARSKI:def 3 :: thesis:
assume y in dom PP ; :: thesis:
then ex z being object st [y,z] in PP by XTUPLE_0:def 12;
hence y in F1 by A5; :: thesis:

end;

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 S₁[f2,k + 1] holds
[(f2 | (k + 1)),f2] in PP

proof

let f2 be Element of ((k + 1) + 1) -tuples_on X; :: thesis:
assume A53: S₁[f2,k + 1] ; :: thesis:
A54: f2 in { F where F is Element of ((k + 1) + 1) -tuples_on X : S₁[F,k + 1] } by A53;
set f1 = f2 | (k + 1);
A55: S₃[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)

proof

let i be Nat; :: thesis:
set i1 = i + 1;
assume A57: i in Seg k ; :: thesis:
then A58: 1 <= i by FINSEQ_1:1;
A59: i <= k by A57, FINSEQ_1:1;
then i < k + 1 by NAT_1:13;
then A60: ( f2 . (i + 1) in P . (f2 . i) & f2 . i = f1 . i ) by A58, FINSEQ_1:1, A53, FUNCT_1:49;
1 <= i + 1 by NAT_1:11;
then i + 1 in Seg (k + 1) by A59, XREAL_1:6, FINSEQ_1:1;
hence f1 . (i + 1) in P . (f1 . i) by A60, FUNCT_1:49; :: thesis:

end;

1 <= k + 1 by NAT_1:11;
then 1 in Seg (k + 1) ;
then S₁[f1,k] by A56, FUNCT_1:49, A53;
then f1 in F1 ;
hence [(f2 | (k + 1)),f2] in PP by A54, A55, A5; :: thesis:

end;

per cases ;

suppose n = 0 ; :: thesis:

then A61: n |^ (k + 1) = 0 by NAT_1:11, NEWTON:11;
then A62: PP is empty by A51;
{ F where F is Element of ((k + 1) + 1) -tuples_on X : S₁[F,k + 1] } is empty

proof

assume not { F where F is Element of ((k + 1) + 1) -tuples_on X : S₁[F,k + 1] } is empty ; :: thesis:
then consider x2 being object such that
A63: x2 in { F where F is Element of ((k + 1) + 1) -tuples_on X : S₁[F,k + 1] } ;
ex f2 being Element of ((k + 1) + 1) -tuples_on X st
( x2 = f2 & S₁[f2,k + 1] ) by A63;
hence contradiction by A52, A62; :: thesis:

end;

hence S₂[k + 1] by A61; :: thesis:

end;

suppose A64: n > 0 ; :: thesis:

defpred S₄[ 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 : S₁[F,k + 1] } & S₄[y,z] )

proof

let y be object ; :: thesis:
assume A66: y in PP ; :: thesis:
then consider y1, y2 being object such that
A67: y = [y1,y2] by RELAT_1:def 1;
take y2 ; :: thesis:
thus ( y2 in { F where F is Element of ((k + 1) + 1) -tuples_on X : S₁[F,k + 1] } & S₄[y,y2] ) by XTUPLE_0:1, A66, A67, A5; :: thesis:

end;

consider pr being Function of PP, { F where F is Element of ((k + 1) + 1) -tuples_on X : S₁[F,k + 1] } such that
A68: for y being object st y in PP holds
S₄[y,pr . y] from FUNCT_2:sch 1(A65);
A69: pr is one-to-one

proof

let x1, x2 be object ; :: according to FUNCT_1:def 4 :: thesis:
assume that
A70: x1 in dom pr and
A71: x2 in dom pr and
A72: pr . x1 = pr . x2 ; :: thesis:
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 : S₁[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
S₁[f1,k + 1] ;
f1 | (k + 1) = y1 by A73, A70, A5, A77;
hence x1 = x2 by A71, A5, A75, A72, A73, A74, A76, A77; :: thesis:

end;

not { F where F is Element of ((k + 1) + 1) -tuples_on X : S₁[F,k + 1] } is empty

proof

n |^ (k + 1) > 0 by NEWTON:83, A64;
then not PP is empty by A51, XREAL_1:129;
then consider x being object such that
A78: x in PP ;
ex y, z being object st x = [y,z] by RELAT_1:def 1, A78;
hence not { F where F is Element of ((k + 1) + 1) -tuples_on X : S₁[F,k + 1] } is empty by A78, A5; :: thesis:

end;

then A79: dom pr = PP by FUNCT_2:def 1;
{ F where F is Element of ((k + 1) + 1) -tuples_on X : S₁[F,k + 1] } c= rng pr

proof

let x2 be object ; :: according to TARSKI:def 3 :: thesis:
assume x2 in { F where F is Element of ((k + 1) + 1) -tuples_on X : S₁[F,k + 1] } ; :: thesis:
then consider f2 being Element of ((k + 1) + 1) -tuples_on X such that
A80: x2 = f2 and
A81: S₁[f2,k + 1] ;
( [(f2 | (k + 1)),f2] in PP & pr . [(f2 | (k + 1)),f2] = f2 ) by A81, A52, A68;
hence x2 in rng pr by A79, FUNCT_1:def 3, A80; :: thesis:

end;

then { F where F is Element of ((k + 1) + 1) -tuples_on X : S₁[F,k + 1] } = rng pr ;
hence S₂[k + 1] by A69, A79, WELLORD2:def 4, A51, CARD_1:5; :: thesis:

end;

A82: S₂[ 0 ]

proof

deffunc H₁( object ) -> set = <*$1*>;
set F0 = { F where F is Element of (0 + 1) -tuples_on X : S₁[F, 0 ] } ;
A83: for x being object st x in A holds
H₁(x) in { F where F is Element of (0 + 1) -tuples_on X : S₁[F, 0 ] }

proof

let x be object ; :: thesis:
assume A84: x in A ; :: thesis:
A85: len H₁(x) = 1 by FINSEQ_1:39;
rng H₁(x) = {x} by FINSEQ_1:38;
then H₁(x) is FinSequence of X by A84, ZFMISC_1:31, FINSEQ_1:def 4;
then reconsider Px = H₁(x) as Element of (0 + 1) -tuples_on X by A85, FINSEQ_2:133;
S₁[Px, 0 ] by FINSEQ_1:40, A84;
hence H₁(x) in { F where F is Element of (0 + 1) -tuples_on X : S₁[F, 0 ] } ; :: thesis:

end;

consider f being Function of A, { F where F is Element of (0 + 1) -tuples_on X : S₁[F, 0 ] } such that
A86: for x being object st x in A holds
f . x = H₁(x) from FUNCT_2:sch 2(A83);
H₁( the Element of A) in { F where F is Element of (0 + 1) -tuples_on X : S₁[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 : S₁[F, 0 ] } c= rng f

proof

let x be object ; :: according to TARSKI:def 3 :: thesis:
assume x in { F where F is Element of (0 + 1) -tuples_on X : S₁[F, 0 ] } ; :: thesis:
then A88: ex F being Element of (0 + 1) -tuples_on X st
( x = F & S₁[F, 0 ] ) ;
then consider y being Element of X such that
A89: x = <*y*> by FINSEQ_2:97;
A90: <*y*> . 1 = y by FINSEQ_1:40;
then f . y = x by A88, A89, A86;
hence x in rng f by A88, A89, A90, A87, FUNCT_1:def 3; :: thesis:

end;

then A91: rng f = { F where F is Element of (0 + 1) -tuples_on X : S₁[F, 0 ] } ;
A92: f is one-to-one

proof

let x1, x2 be object ; :: according to FUNCT_1:def 4 :: thesis:
assume that
A93: ( x1 in dom f & x2 in dom f ) and
A94: f . x1 = f . x2 ; :: thesis:
A95: ( f . x1 = H₁(x1) & f . x2 = H₁(x2) ) by A93, A86;
H₁(x1) . 1 = x1 by FINSEQ_1:40;
hence x1 = x2 by A95, FINSEQ_1:40, A94; :: thesis:

end;

n |^ 0 = 1 by NEWTON:4;
hence S₂[ 0 ] by A91, WELLORD2:def 4, A87, A92, CARD_1:5; :: thesis:

end;

for k being Nat holds S₂[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) ; :: thesis: