let T be binary Tree; :: thesis:
let t be Element of T; :: thesis:
defpred S₁[ FinSequence] means ( $1 is Element of T implies rng $1 c= BOOLEAN );
A1: for p being FinSequence of NAT
for x being Element of NAT st S₁[p] holds
S₁[p ^ <*x*>]

let p be FinSequence of NAT ; :: thesis:
let x be Element of NAT ; :: thesis:
assume A2: S₁[p] ; :: thesis:
assume A3: p ^ <*x*> is Element of T ; :: thesis:
then reconsider p1 = p as Element of T by TREES_1:21;
p ^ <*x*> in { (p ^ <*n*>) where n is Nat : p ^ <*n*> in T } by A3;
then A4: p ^ <*x*> in succ p1 by TREES_2:def 5;
then not p in Leaves T by BINTREE1:3;
then succ p1 = {(p ^ <*0*>),(p ^ <*1*>)} by BINTREE1:def 2;
then ( p ^ <*x*> = p ^ <*0*> or p ^ <*x*> = p ^ <*1*> ) by A4, TARSKI:def 2;
then ( x = 0 or x = 1 ) by FINSEQ_2:17;
then A5: x in {0,1} by TARSKI:def 2;
A6: {x} c= BOOLEAN by A5, TARSKI:def 1;
rng <*x*> = {x} by FINSEQ_1:38;
then (rng p) \/ (rng <*x*>) c= BOOLEAN by A2, A3, A6, TREES_1:21, XBOOLE_1:8;
hence rng (p ^ <*x*>) c= BOOLEAN by FINSEQ_1:31; :: thesis:

end;

A7: S₁[ <*> NAT] by XBOOLE_1:2;
for p being FinSequence of NAT holds S₁[p] from FINSEQ_2:sch 2(A7, A1);
then rng t c= BOOLEAN ;
hence t is FinSequence of BOOLEAN by FINSEQ_1:def 4; :: thesis: