let D be non empty finite set ; :: thesis: ex B being FinSequence of bool D st
( len B = card D & B is ascending & B is terms've_same_card_as_number )
defpred S₁[ Element of NAT ] means for D being non empty finite set st card D = $1 holds
ex B being FinSequence of bool D st
( len B = card D & B is ascending & B is terms've_same_card_as_number );
A1: for n being Element of NAT st S₁[n] holds
S₁[n + 1]

proof

let n be Element of NAT ; :: thesis: ( S₁[n] implies S₁[n + 1] )
assume A2: S₁[n] ; :: thesis: S₁[n + 1]
let D be non empty finite set ; :: thesis: ( card D = n + 1 implies ex B being FinSequence of bool D st
( len B = card D & B is ascending & B is terms've_same_card_as_number ) )
assume A3: card D = n + 1 ; :: thesis: ex B being FinSequence of bool D st
( len B = card D & B is ascending & B is terms've_same_card_as_number )
set x = the Element of D;
set Y = D \ { the Element of D};
{ the Element of D} c= D by ZFMISC_1:31;
then A4: card (D \ { the Element of D}) = (card D) - (card { the Element of D}) by CARD_2:44
.= (n + 1) - 1 by A3, CARD_1:30
.= n ;

now

per cases ( n = 0 or n <> 0 ) ;

case A5: n = 0 ; :: thesis: ex f being FinSequence of bool D st
( card D = len f & f is ascending & f is terms've_same_card_as_number )

set f = <*D*>;
A6: len <*D*> = 1 by FINSEQ_1:39;
A7: rng <*D*> = {D} by FINSEQ_1:39;
rng <*D*> c= bool D

proof

let z be set ; :: according to TARSKI:def 3 :: thesis: ( not z in rng <*D*> or z in bool D )
assume z in rng <*D*> ; :: thesis: z in bool D
then z = D by A7, TARSKI:def 1;
hence z in bool D by ZFMISC_1:def 1; :: thesis: verum

end;

then reconsider f = <*D*> as FinSequence of bool D by FINSEQ_1:def 4;
take f = f; :: thesis: ( card D = len f & f is ascending & f is terms've_same_card_as_number )
thus card D = len f by A3, A5, FINSEQ_1:40; :: thesis: ( f is ascending & f is terms've_same_card_as_number )
thus f is ascending :: thesis: f is terms've_same_card_as_number

proof

let m be Nat; :: according to REARRAN1:def 2 :: thesis: ( 1 <= m & m <= (len f) - 1 implies f . m c= f . (m + 1) )
assume ( 1 <= m & m <= (len f) - 1 ) ; :: thesis: f . m c= f . (m + 1)
hence f . m c= f . (m + 1) by A6, XXREAL_0:2; :: thesis: verum

end;

thus f is terms've_same_card_as_number :: thesis: verum

proof

let m be Nat; :: according to REARRAN1:def 1 :: thesis: ( 1 <= m & m <= len f implies for B being finite set st B = f . m holds
card B = m )
assume ( 1 <= m & m <= len f ) ; :: thesis: for B being finite set st B = f . m holds
card B = m
then A8: m = 1 by A6, XXREAL_0:1;
let B be finite set ; :: thesis: ( B = f . m implies card B = m )
assume B = f . m ; :: thesis: card B = m
hence card B = m by A3, A5, A8, FINSEQ_1:40; :: thesis: verum

end;

end;

case n <> 0 ; :: thesis: ex g being FinSequence of bool D st
( len g = card D & g is ascending & g is terms've_same_card_as_number )

then reconsider Y = D \ { the Element of D} as non empty finite set by A4;
D in bool D by ZFMISC_1:def 1;
then A9: {D} c= bool D by ZFMISC_1:31;
consider f being FinSequence of bool Y such that
A10: len f = card Y and
A11: f is ascending and
A12: f is terms've_same_card_as_number by A2, A4;
set g = f ^ <*D*>;
A13: ( rng <*D*> = {D} & rng (f ^ <*D*>) = (rng f) \/ (rng <*D*>) ) by FINSEQ_1:31, FINSEQ_1:39;
bool Y c= bool D by ZFMISC_1:67;
then rng f c= bool D by XBOOLE_1:1;
then rng (f ^ <*D*>) c= (bool D) \/ (bool D) by A9, A13, XBOOLE_1:13;
then reconsider g = f ^ <*D*> as FinSequence of bool D by FINSEQ_1:def 4;
take g = g; :: thesis: ( len g = card D & g is ascending & g is terms've_same_card_as_number )
A14: len <*D*> = 1 by FINSEQ_1:39;
then A15: len g = (len f) + 1 by FINSEQ_1:22;
thus len g = card D by A3, A4, A10, A14, FINSEQ_1:22; :: thesis: ( g is ascending & g is terms've_same_card_as_number )
thus g is ascending :: thesis: g is terms've_same_card_as_number

proof

let m be Nat; :: according to REARRAN1:def 2 :: thesis: ( 1 <= m & m <= (len g) - 1 implies g . m c= g . (m + 1) )
assume that
A16: 1 <= m and
A17: m <= (len g) - 1 ; :: thesis: g . m c= g . (m + 1)
m in dom f by A15, A16, A17, FINSEQ_3:25;
then A18: g . m = f . m by FINSEQ_1:def 7;

per cases ( m = len f or m <> len f ) ;

suppose A19: m = len f ; :: thesis: g . m c= g . (m + 1)

then reconsider gm = g . m as finite set by A16, A18, Lm2;
( gm = Y & g . (m + 1) = D ) by A10, A12, A18, A19, Lm3, FINSEQ_1:42;
hence g . m c= g . (m + 1) ; :: thesis: verum

end;

suppose m <> len f ; :: thesis: g . m c= g . (m + 1)

then m < len f by A15, A17, XXREAL_0:1;
then A20: m + 1 <= len f by NAT_1:13;
1 <= m + 1 by A16, NAT_1:13;
then m + 1 in dom f by A20, FINSEQ_3:25;
then A21: g . (m + 1) = f . (m + 1) by FINSEQ_1:def 7;
m <= (len f) - 1 by A20, XREAL_1:19;
hence g . m c= g . (m + 1) by A11, A16, A18, A21, Def2; :: thesis: verum

end;

end;

end;

thus g is terms've_same_card_as_number :: thesis: verum

proof

let m be Nat; :: according to REARRAN1:def 1 :: thesis: ( 1 <= m & m <= len g implies for B being finite set st B = g . m holds
card B = m )
assume that
A22: 1 <= m and
A23: m <= len g ; :: thesis: for B being finite set st B = g . m holds
card B = m
let B be finite set ; :: thesis: ( B = g . m implies card B = m )
assume A24: B = g . m ; :: thesis: card B = m

per cases ( m = len g or m <> len g ) ;

suppose m = len g ; :: thesis: card B = m

hence card B = m by A3, A4, A10, A15, A24, FINSEQ_1:42; :: thesis: verum

end;

suppose m <> len g ; :: thesis: card B = m

then m < len g by A23, XXREAL_0:1;
then A25: m <= len f by A15, NAT_1:13;
then m in dom f by A22, FINSEQ_3:25;
then g . m = f . m by FINSEQ_1:def 7;
hence card B = m by A12, A22, A24, A25, Def1; :: thesis: verum

end;

end;

end;

end;

end;

end;

hence ex B being FinSequence of bool D st
( len B = card D & B is ascending & B is terms've_same_card_as_number ) ; :: thesis: verum

end;

A26: S₁[ 0 ] ;
for n being Element of NAT holds S₁[n] from NAT_1:sch 1(A26, A1);
hence ex B being FinSequence of bool D st
( len B = card D & B is ascending & B is terms've_same_card_as_number ) ; :: thesis: verum