let T be full Tree; :: thesis: for n being Nat holds card (T -level n) = 2 to_power n

defpred S_{1}[ Nat] means card (T -level $1) = 2 to_power $1;

A1: T = {0,1} * by Def2;

A2: for n being Nat st S_{1}[n] holds

S_{1}[n + 1]

.= 1 by CARD_1:30

.= 2 to_power 0 by POWER:24 ;

then A53: S_{1}[ 0 ]
;

thus for n being Nat holds S_{1}[n]
from NAT_1:sch 2(A53, A2); :: thesis: verum

defpred S

A1: T = {0,1} * by Def2;

A2: for n being Nat st S

S

proof

card (T -level 0) =
card {{}}
by TREES_9:44
defpred S_{2}[ set , set ] means ex p being FinSequence st

( p = $1 & $2 = p ^ <*0*> );

let n be Nat; :: thesis: ( S_{1}[n] implies S_{1}[n + 1] )

set Tn10 = { p where p is Element of T : ( len p = n + 1 & p . (n + 1) = 0 ) } ;

set Tn11 = { p where p is Element of T : ( len p = n + 1 & p . (n + 1) = 1 ) } ;

A3: (0* (n + 1)) . (n + 1) = 0 by FINSEQ_1:4, FUNCOP_1:7;

( len (0* (n + 1)) = n + 1 & 0* (n + 1) in T ) by A1, BINARI_3:4, CARD_1:def 7;

then A4: 0* (n + 1) in { p where p is Element of T : ( len p = n + 1 & p . (n + 1) = 0 ) } by A3;

A5: { p where p is Element of T : ( len p = n + 1 & p . (n + 1) = 1 ) } c= T -level (n + 1)

defpred S_{3}[ set , set ] means ex p being FinSequence st

( p = $1 & $2 = p ^ <*1*> );

A9: { p where p is Element of T : ( len p = n + 1 & p . (n + 1) = 0 ) } c= T -level (n + 1)

then 0* n is FinSequence of {0,1} by FINSEQ_1:def 11;

then (0* n) ^ <*1*> is FinSequence of {0,1} by A8, Lm1;

then A12: (0* n) ^ <*1*> in T by A1, FINSEQ_1:def 11;

reconsider Tn = T -level n as non empty finite set by A1, Th10;

assume A13: card (T -level n) = 2 to_power n ; :: thesis: S_{1}[n + 1]

len (0* n) = n by CARD_1:def 7;

then A14: ((0* n) ^ <*1*>) . (n + 1) = 1 by FINSEQ_1:42;

len ((0* n) ^ <*1*>) = (len (0* n)) + 1 by FINSEQ_2:16

.= n + 1 by CARD_1:def 7 ;

then (0* n) ^ <*1*> in { p where p is Element of T : ( len p = n + 1 & p . (n + 1) = 1 ) } by A12, A14;

then reconsider Tn10 = { p where p is Element of T : ( len p = n + 1 & p . (n + 1) = 0 ) } , Tn11 = { p where p is Element of T : ( len p = n + 1 & p . (n + 1) = 1 ) } as non empty finite set by A4, A9, A5;

A15: Tn10 \/ Tn11 c= T -level (n + 1) by A9, A5, XBOOLE_1:8;

A16: for x being Element of Tn ex y being Element of Tn11 st S_{3}[x,y]

A20: for x being Element of Tn holds S_{3}[x,f1 . x]
from FUNCT_2:sch 3(A16);

A28: for x being Element of Tn ex y being Element of Tn10 st S_{2}[x,y]

A32: for x being Element of Tn holds S_{2}[x,f0 . x]
from FUNCT_2:sch 3(A28);

then Tn,f1 .: Tn are_equipotent by CARD_1:33;

then A35: Tn, rng f1 are_equipotent by RELSET_1:22;

A36: T -level (n + 1) c= Tn10 \/ Tn11

then Tn,f0 .: Tn are_equipotent by CARD_1:33;

then Tn, rng f0 are_equipotent by RELSET_1:22;

then A49: card Tn = card Tn10 by A46, CARD_1:5;

A50: Tn10 misses Tn11

.= 2 * (2 to_power n) by POWER:25

.= (card Tn) + (card Tn) by A13

.= (card Tn10) + (card Tn11) by A49, A35, A27, CARD_1:5

.= card (Tn10 \/ Tn11) by A50, CARD_2:40

.= card (T -level (n + 1)) by A15, A36, XBOOLE_0:def 10 ; :: thesis: verum

end;( p = $1 & $2 = p ^ <*0*> );

let n be Nat; :: thesis: ( S

set Tn10 = { p where p is Element of T : ( len p = n + 1 & p . (n + 1) = 0 ) } ;

set Tn11 = { p where p is Element of T : ( len p = n + 1 & p . (n + 1) = 1 ) } ;

A3: (0* (n + 1)) . (n + 1) = 0 by FINSEQ_1:4, FUNCOP_1:7;

( len (0* (n + 1)) = n + 1 & 0* (n + 1) in T ) by A1, BINARI_3:4, CARD_1:def 7;

then A4: 0* (n + 1) in { p where p is Element of T : ( len p = n + 1 & p . (n + 1) = 0 ) } by A3;

A5: { p where p is Element of T : ( len p = n + 1 & p . (n + 1) = 1 ) } c= T -level (n + 1)

proof

rng <*1*> c= {0,1}
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { p where p is Element of T : ( len p = n + 1 & p . (n + 1) = 1 ) } or x in T -level (n + 1) )

assume x in { p where p is Element of T : ( len p = n + 1 & p . (n + 1) = 1 ) } ; :: thesis: x in T -level (n + 1)

then consider p being Element of T such that

A6: p = x and

A7: len p = n + 1 and

p . (n + 1) = 1 ;

p in { w where w is Element of T : len w = n + 1 } by A7;

hence x in T -level (n + 1) by A6, TREES_2:def 6; :: thesis: verum

end;assume x in { p where p is Element of T : ( len p = n + 1 & p . (n + 1) = 1 ) } ; :: thesis: x in T -level (n + 1)

then consider p being Element of T such that

A6: p = x and

A7: len p = n + 1 and

p . (n + 1) = 1 ;

p in { w where w is Element of T : len w = n + 1 } by A7;

hence x in T -level (n + 1) by A6, TREES_2:def 6; :: thesis: verum

proof

then A8:
<*1*> is FinSequence of {0,1}
by FINSEQ_1:def 4;
let z be object ; :: according to TARSKI:def 3 :: thesis: ( not z in rng <*1*> or z in {0,1} )

assume z in rng <*1*> ; :: thesis: z in {0,1}

then z in {1} by FINSEQ_1:38;

then z = 1 by TARSKI:def 1;

hence z in {0,1} by TARSKI:def 2; :: thesis: verum

end;assume z in rng <*1*> ; :: thesis: z in {0,1}

then z in {1} by FINSEQ_1:38;

then z = 1 by TARSKI:def 1;

hence z in {0,1} by TARSKI:def 2; :: thesis: verum

defpred S

( p = $1 & $2 = p ^ <*1*> );

A9: { p where p is Element of T : ( len p = n + 1 & p . (n + 1) = 0 ) } c= T -level (n + 1)

proof

0* n in {0,1} *
by BINARI_3:4;
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { p where p is Element of T : ( len p = n + 1 & p . (n + 1) = 0 ) } or x in T -level (n + 1) )

assume x in { p where p is Element of T : ( len p = n + 1 & p . (n + 1) = 0 ) } ; :: thesis: x in T -level (n + 1)

then consider p being Element of T such that

A10: p = x and

A11: len p = n + 1 and

p . (n + 1) = 0 ;

p in { w where w is Element of T : len w = n + 1 } by A11;

hence x in T -level (n + 1) by A10, TREES_2:def 6; :: thesis: verum

end;assume x in { p where p is Element of T : ( len p = n + 1 & p . (n + 1) = 0 ) } ; :: thesis: x in T -level (n + 1)

then consider p being Element of T such that

A10: p = x and

A11: len p = n + 1 and

p . (n + 1) = 0 ;

p in { w where w is Element of T : len w = n + 1 } by A11;

hence x in T -level (n + 1) by A10, TREES_2:def 6; :: thesis: verum

then 0* n is FinSequence of {0,1} by FINSEQ_1:def 11;

then (0* n) ^ <*1*> is FinSequence of {0,1} by A8, Lm1;

then A12: (0* n) ^ <*1*> in T by A1, FINSEQ_1:def 11;

reconsider Tn = T -level n as non empty finite set by A1, Th10;

assume A13: card (T -level n) = 2 to_power n ; :: thesis: S

len (0* n) = n by CARD_1:def 7;

then A14: ((0* n) ^ <*1*>) . (n + 1) = 1 by FINSEQ_1:42;

len ((0* n) ^ <*1*>) = (len (0* n)) + 1 by FINSEQ_2:16

.= n + 1 by CARD_1:def 7 ;

then (0* n) ^ <*1*> in { p where p is Element of T : ( len p = n + 1 & p . (n + 1) = 1 ) } by A12, A14;

then reconsider Tn10 = { p where p is Element of T : ( len p = n + 1 & p . (n + 1) = 0 ) } , Tn11 = { p where p is Element of T : ( len p = n + 1 & p . (n + 1) = 1 ) } as non empty finite set by A4, A9, A5;

A15: Tn10 \/ Tn11 c= T -level (n + 1) by A9, A5, XBOOLE_1:8;

A16: for x being Element of Tn ex y being Element of Tn11 st S

proof

consider f1 being Function of Tn,Tn11 such that
let x be Element of Tn; :: thesis: ex y being Element of Tn11 st S_{3}[x,y]

x in T -level n ;

then x in { w where w is Element of T : len w = n } by TREES_2:def 6;

then consider p being Element of T such that

A17: p = x and

A18: len p = n ;

set y = p ^ <*1*>;

p ^ <*1*> is FinSequence of {0,1} by A8, Lm1;

then A19: p ^ <*1*> in T by A1, FINSEQ_1:def 11;

( len (p ^ <*1*>) = n + 1 & (p ^ <*1*>) . (n + 1) = 1 ) by A18, FINSEQ_1:42, FINSEQ_2:16;

then p ^ <*1*> in { t where t is Element of T : ( len t = n + 1 & t . (n + 1) = 1 ) } by A19;

then reconsider y = p ^ <*1*> as Element of Tn11 ;

take y ; :: thesis: S_{3}[x,y]

take p ; :: thesis: ( p = x & y = p ^ <*1*> )

thus ( p = x & y = p ^ <*1*> ) by A17; :: thesis: verum

end;x in T -level n ;

then x in { w where w is Element of T : len w = n } by TREES_2:def 6;

then consider p being Element of T such that

A17: p = x and

A18: len p = n ;

set y = p ^ <*1*>;

p ^ <*1*> is FinSequence of {0,1} by A8, Lm1;

then A19: p ^ <*1*> in T by A1, FINSEQ_1:def 11;

( len (p ^ <*1*>) = n + 1 & (p ^ <*1*>) . (n + 1) = 1 ) by A18, FINSEQ_1:42, FINSEQ_2:16;

then p ^ <*1*> in { t where t is Element of T : ( len t = n + 1 & t . (n + 1) = 1 ) } by A19;

then reconsider y = p ^ <*1*> as Element of Tn11 ;

take y ; :: thesis: S

take p ; :: thesis: ( p = x & y = p ^ <*1*> )

thus ( p = x & y = p ^ <*1*> ) by A17; :: thesis: verum

A20: for x being Element of Tn holds S

now :: thesis: for y being object st y in Tn11 holds

ex x being object st

( x in Tn & y = f1 . x )

then A27:
rng f1 = Tn11
by FUNCT_2:10;ex x being object st

( x in Tn & y = f1 . x )

let y be object ; :: thesis: ( y in Tn11 implies ex x being object st

( x in Tn & y = f1 . x ) )

assume y in Tn11 ; :: thesis: ex x being object st

( x in Tn & y = f1 . x )

then consider t being Element of T such that

A21: t = y and

A22: len t = n + 1 and

A23: t . (n + 1) = 1 ;

consider p being FinSequence of BOOLEAN , d being Element of BOOLEAN such that

A24: t = p ^ <*d*> by A22, FINSEQ_2:19;

reconsider x = p as object ;

take x = x; :: thesis: ( x in Tn & y = f1 . x )

A25: (len p) + 1 = n + 1 by A22, A24, FINSEQ_2:16;

p in T by A1, FINSEQ_1:def 11;

then A26: p in { w where w is Element of T : len w = n } by A25;

hence x in Tn by TREES_2:def 6; :: thesis: y = f1 . x

reconsider x9 = x as Element of Tn by A26, TREES_2:def 6;

ex q being FinSequence st

( q = x9 & f1 . x9 = q ^ <*1*> ) by A20;

hence y = f1 . x by A21, A23, A24, A25, FINSEQ_1:42; :: thesis: verum

end;( x in Tn & y = f1 . x ) )

assume y in Tn11 ; :: thesis: ex x being object st

( x in Tn & y = f1 . x )

then consider t being Element of T such that

A21: t = y and

A22: len t = n + 1 and

A23: t . (n + 1) = 1 ;

consider p being FinSequence of BOOLEAN , d being Element of BOOLEAN such that

A24: t = p ^ <*d*> by A22, FINSEQ_2:19;

reconsider x = p as object ;

take x = x; :: thesis: ( x in Tn & y = f1 . x )

A25: (len p) + 1 = n + 1 by A22, A24, FINSEQ_2:16;

p in T by A1, FINSEQ_1:def 11;

then A26: p in { w where w is Element of T : len w = n } by A25;

hence x in Tn by TREES_2:def 6; :: thesis: y = f1 . x

reconsider x9 = x as Element of Tn by A26, TREES_2:def 6;

ex q being FinSequence st

( q = x9 & f1 . x9 = q ^ <*1*> ) by A20;

hence y = f1 . x by A21, A23, A24, A25, FINSEQ_1:42; :: thesis: verum

A28: for x being Element of Tn ex y being Element of Tn10 st S

proof

consider f0 being Function of Tn,Tn10 such that
let x be Element of Tn; :: thesis: ex y being Element of Tn10 st S_{2}[x,y]

x in T -level n ;

then x in { w where w is Element of T : len w = n } by TREES_2:def 6;

then consider p being Element of T such that

A29: p = x and

A30: len p = n ;

set y = p ^ <*0*>;

rng <*0*> c= {0,1}

then p ^ <*0*> is FinSequence of {0,1} by Lm1;

then A31: p ^ <*0*> in T by A1, FINSEQ_1:def 11;

( len (p ^ <*0*>) = n + 1 & (p ^ <*0*>) . (n + 1) = 0 ) by A30, FINSEQ_1:42, FINSEQ_2:16;

then p ^ <*0*> in { t where t is Element of T : ( len t = n + 1 & t . (n + 1) = 0 ) } by A31;

then reconsider y = p ^ <*0*> as Element of Tn10 ;

take y ; :: thesis: S_{2}[x,y]

take p ; :: thesis: ( p = x & y = p ^ <*0*> )

thus ( p = x & y = p ^ <*0*> ) by A29; :: thesis: verum

end;x in T -level n ;

then x in { w where w is Element of T : len w = n } by TREES_2:def 6;

then consider p being Element of T such that

A29: p = x and

A30: len p = n ;

set y = p ^ <*0*>;

rng <*0*> c= {0,1}

proof

then
<*0*> is FinSequence of {0,1}
by FINSEQ_1:def 4;
let z be object ; :: according to TARSKI:def 3 :: thesis: ( not z in rng <*0*> or z in {0,1} )

assume z in rng <*0*> ; :: thesis: z in {0,1}

then z in {0} by FINSEQ_1:38;

then z = 0 by TARSKI:def 1;

hence z in {0,1} by TARSKI:def 2; :: thesis: verum

end;assume z in rng <*0*> ; :: thesis: z in {0,1}

then z in {0} by FINSEQ_1:38;

then z = 0 by TARSKI:def 1;

hence z in {0,1} by TARSKI:def 2; :: thesis: verum

then p ^ <*0*> is FinSequence of {0,1} by Lm1;

then A31: p ^ <*0*> in T by A1, FINSEQ_1:def 11;

( len (p ^ <*0*>) = n + 1 & (p ^ <*0*>) . (n + 1) = 0 ) by A30, FINSEQ_1:42, FINSEQ_2:16;

then p ^ <*0*> in { t where t is Element of T : ( len t = n + 1 & t . (n + 1) = 0 ) } by A31;

then reconsider y = p ^ <*0*> as Element of Tn10 ;

take y ; :: thesis: S

take p ; :: thesis: ( p = x & y = p ^ <*0*> )

thus ( p = x & y = p ^ <*0*> ) by A29; :: thesis: verum

A32: for x being Element of Tn holds S

now :: thesis: for x1, x2 being object st x1 in dom f1 & x2 in dom f1 & f1 . x1 = f1 . x2 holds

x1 = x2

then
( Tn c= dom f1 & f1 is one-to-one )
by FUNCT_1:def 4, FUNCT_2:def 1;x1 = x2

let x1, x2 be object ; :: thesis: ( x1 in dom f1 & x2 in dom f1 & f1 . x1 = f1 . x2 implies x1 = x2 )

assume that

A33: ( x1 in dom f1 & x2 in dom f1 ) and

A34: f1 . x1 = f1 . x2 ; :: thesis: x1 = x2

reconsider x19 = x1, x29 = x2 as Element of Tn by A33, FUNCT_2:def 1;

( ex p1 being FinSequence st

( p1 = x19 & f1 . x19 = p1 ^ <*1*> ) & ex p2 being FinSequence st

( p2 = x29 & f1 . x29 = p2 ^ <*1*> ) ) by A20;

hence x1 = x2 by A34, FINSEQ_2:17; :: thesis: verum

end;assume that

A33: ( x1 in dom f1 & x2 in dom f1 ) and

A34: f1 . x1 = f1 . x2 ; :: thesis: x1 = x2

reconsider x19 = x1, x29 = x2 as Element of Tn by A33, FUNCT_2:def 1;

( ex p1 being FinSequence st

( p1 = x19 & f1 . x19 = p1 ^ <*1*> ) & ex p2 being FinSequence st

( p2 = x29 & f1 . x29 = p2 ^ <*1*> ) ) by A20;

hence x1 = x2 by A34, FINSEQ_2:17; :: thesis: verum

then Tn,f1 .: Tn are_equipotent by CARD_1:33;

then A35: Tn, rng f1 are_equipotent by RELSET_1:22;

A36: T -level (n + 1) c= Tn10 \/ Tn11

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in T -level (n + 1) or x in Tn10 \/ Tn11 )

assume x in T -level (n + 1) ; :: thesis: x in Tn10 \/ Tn11

then x in { w where w is Element of T : len w = n + 1 } by TREES_2:def 6;

then consider p being Element of T such that

A37: p = x and

A38: len p = n + 1 ;

( x in Tn10 or x in Tn11 )

end;assume x in T -level (n + 1) ; :: thesis: x in Tn10 \/ Tn11

then x in { w where w is Element of T : len w = n + 1 } by TREES_2:def 6;

then consider p being Element of T such that

A37: p = x and

A38: len p = n + 1 ;

( x in Tn10 or x in Tn11 )

proof

hence
x in Tn10 \/ Tn11
by XBOOLE_0:def 3; :: thesis: verum
n + 1 in Seg (n + 1)
by FINSEQ_1:4;

then n + 1 in dom p by A38, FINSEQ_1:def 3;

then p . (n + 1) in BOOLEAN by FINSEQ_2:11;

then A39: ( p . (n + 1) = 0 or p . (n + 1) = 1 ) by TARSKI:def 2;

assume not x in Tn10 ; :: thesis: x in Tn11

hence x in Tn11 by A37, A38, A39; :: thesis: verum

end;then n + 1 in dom p by A38, FINSEQ_1:def 3;

then p . (n + 1) in BOOLEAN by FINSEQ_2:11;

then A39: ( p . (n + 1) = 0 or p . (n + 1) = 1 ) by TARSKI:def 2;

assume not x in Tn10 ; :: thesis: x in Tn11

hence x in Tn11 by A37, A38, A39; :: thesis: verum

now :: thesis: for y being object st y in Tn10 holds

ex x being object st

( x in Tn & y = f0 . x )

then A46:
rng f0 = Tn10
by FUNCT_2:10;ex x being object st

( x in Tn & y = f0 . x )

let y be object ; :: thesis: ( y in Tn10 implies ex x being object st

( x in Tn & y = f0 . x ) )

assume y in Tn10 ; :: thesis: ex x being object st

( x in Tn & y = f0 . x )

then consider t being Element of T such that

A40: t = y and

A41: len t = n + 1 and

A42: t . (n + 1) = 0 ;

consider p being FinSequence of BOOLEAN , d being Element of BOOLEAN such that

A43: t = p ^ <*d*> by A41, FINSEQ_2:19;

reconsider x = p as object ;

take x = x; :: thesis: ( x in Tn & y = f0 . x )

A44: (len p) + 1 = n + 1 by A41, A43, FINSEQ_2:16;

p in T by A1, FINSEQ_1:def 11;

then A45: p in { w where w is Element of T : len w = n } by A44;

hence x in Tn by TREES_2:def 6; :: thesis: y = f0 . x

reconsider x9 = x as Element of Tn by A45, TREES_2:def 6;

ex q being FinSequence st

( q = x9 & f0 . x9 = q ^ <*0*> ) by A32;

hence y = f0 . x by A40, A42, A43, A44, FINSEQ_1:42; :: thesis: verum

end;( x in Tn & y = f0 . x ) )

assume y in Tn10 ; :: thesis: ex x being object st

( x in Tn & y = f0 . x )

then consider t being Element of T such that

A40: t = y and

A41: len t = n + 1 and

A42: t . (n + 1) = 0 ;

consider p being FinSequence of BOOLEAN , d being Element of BOOLEAN such that

A43: t = p ^ <*d*> by A41, FINSEQ_2:19;

reconsider x = p as object ;

take x = x; :: thesis: ( x in Tn & y = f0 . x )

A44: (len p) + 1 = n + 1 by A41, A43, FINSEQ_2:16;

p in T by A1, FINSEQ_1:def 11;

then A45: p in { w where w is Element of T : len w = n } by A44;

hence x in Tn by TREES_2:def 6; :: thesis: y = f0 . x

reconsider x9 = x as Element of Tn by A45, TREES_2:def 6;

ex q being FinSequence st

( q = x9 & f0 . x9 = q ^ <*0*> ) by A32;

hence y = f0 . x by A40, A42, A43, A44, FINSEQ_1:42; :: thesis: verum

now :: thesis: for x1, x2 being object st x1 in dom f0 & x2 in dom f0 & f0 . x1 = f0 . x2 holds

x1 = x2

then
( Tn c= dom f0 & f0 is one-to-one )
by FUNCT_1:def 4, FUNCT_2:def 1;x1 = x2

let x1, x2 be object ; :: thesis: ( x1 in dom f0 & x2 in dom f0 & f0 . x1 = f0 . x2 implies x1 = x2 )

assume that

A47: ( x1 in dom f0 & x2 in dom f0 ) and

A48: f0 . x1 = f0 . x2 ; :: thesis: x1 = x2

reconsider x19 = x1, x29 = x2 as Element of Tn by A47, FUNCT_2:def 1;

( ex p1 being FinSequence st

( p1 = x19 & f0 . x19 = p1 ^ <*0*> ) & ex p2 being FinSequence st

( p2 = x29 & f0 . x29 = p2 ^ <*0*> ) ) by A32;

hence x1 = x2 by A48, FINSEQ_2:17; :: thesis: verum

end;assume that

A47: ( x1 in dom f0 & x2 in dom f0 ) and

A48: f0 . x1 = f0 . x2 ; :: thesis: x1 = x2

reconsider x19 = x1, x29 = x2 as Element of Tn by A47, FUNCT_2:def 1;

( ex p1 being FinSequence st

( p1 = x19 & f0 . x19 = p1 ^ <*0*> ) & ex p2 being FinSequence st

( p2 = x29 & f0 . x29 = p2 ^ <*0*> ) ) by A32;

hence x1 = x2 by A48, FINSEQ_2:17; :: thesis: verum

then Tn,f0 .: Tn are_equipotent by CARD_1:33;

then Tn, rng f0 are_equipotent by RELSET_1:22;

then A49: card Tn = card Tn10 by A46, CARD_1:5;

A50: Tn10 misses Tn11

proof

thus 2 to_power (n + 1) =
(2 to_power n) * (2 to_power 1)
by POWER:27
assume
Tn10 /\ Tn11 <> {}
; :: according to XBOOLE_0:def 7 :: thesis: contradiction

then consider x being object such that

A51: x in Tn10 /\ Tn11 by XBOOLE_0:def 1;

x in Tn11 by A51, XBOOLE_0:def 4;

then A52: ex p2 being Element of T st

( p2 = x & len p2 = n + 1 & p2 . (n + 1) = 1 ) ;

x in Tn10 by A51, XBOOLE_0:def 4;

then ex p1 being Element of T st

( p1 = x & len p1 = n + 1 & p1 . (n + 1) = 0 ) ;

hence contradiction by A52; :: thesis: verum

end;then consider x being object such that

A51: x in Tn10 /\ Tn11 by XBOOLE_0:def 1;

x in Tn11 by A51, XBOOLE_0:def 4;

then A52: ex p2 being Element of T st

( p2 = x & len p2 = n + 1 & p2 . (n + 1) = 1 ) ;

x in Tn10 by A51, XBOOLE_0:def 4;

then ex p1 being Element of T st

( p1 = x & len p1 = n + 1 & p1 . (n + 1) = 0 ) ;

hence contradiction by A52; :: thesis: verum

.= 2 * (2 to_power n) by POWER:25

.= (card Tn) + (card Tn) by A13

.= (card Tn10) + (card Tn11) by A49, A35, A27, CARD_1:5

.= card (Tn10 \/ Tn11) by A50, CARD_2:40

.= card (T -level (n + 1)) by A15, A36, XBOOLE_0:def 10 ; :: thesis: verum

.= 1 by CARD_1:30

.= 2 to_power 0 by POWER:24 ;

then A53: S

thus for n being Nat holds S