let T be binary Tree; :: thesis: for t being Element of T holds t is FinSequence of BOOLEAN
let t be Element of T; :: thesis: t is FinSequence of BOOLEAN
defpred S1[ 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 S1[p] holds
S1[p ^ <*x*>]
proof
let p be FinSequence of NAT ; :: thesis: for x being Element of NAT st S1[p] holds
S1[p ^ <*x*>]

let x be Element of NAT ; :: thesis: ( S1[p] implies S1[p ^ <*x*>] )
assume A2: S1[p] ; :: thesis: S1[p ^ <*x*>]
assume A3: p ^ <*x*> is Element of T ; :: thesis: rng (p ^ <*x*>) c= BOOLEAN
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 ^ <*1*>)} by BINTREE1:def 2;
then ( p ^ <*x*> = p ^ or p ^ <*x*> = p ^ <*1*> ) by ;
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 ;
rng <*x*> = {x} by FINSEQ_1:38;
then (rng p) \/ () c= BOOLEAN by ;
hence rng (p ^ <*x*>) c= BOOLEAN by FINSEQ_1:31; :: thesis: verum
end;
A7: S1[ <*> NAT] by XBOOLE_1:2;
for p being FinSequence of NAT holds S1[p] from then rng t c= BOOLEAN ;
hence t is FinSequence of BOOLEAN by FINSEQ_1:def 4; :: thesis: verum