let T be binary Tree; :: thesis: for n being Nat

for t being Element of T st t in T -level n holds

t is Element of n -tuples_on BOOLEAN

let n be Nat; :: thesis: for t being Element of T st t in T -level n holds

t is Element of n -tuples_on BOOLEAN

let t be Element of T; :: thesis: ( t in T -level n implies t is Element of n -tuples_on BOOLEAN )

assume t in T -level n ; :: thesis: t is Element of n -tuples_on BOOLEAN

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

then ex t2 being Element of T st

( t2 = t & len t2 = n ) ;

hence t is Element of n -tuples_on BOOLEAN by FINSEQ_2:92; :: thesis: verum

for t being Element of T st t in T -level n holds

t is Element of n -tuples_on BOOLEAN

let n be Nat; :: thesis: for t being Element of T st t in T -level n holds

t is Element of n -tuples_on BOOLEAN

let t be Element of T; :: thesis: ( t in T -level n implies t is Element of n -tuples_on BOOLEAN )

assume t in T -level n ; :: thesis: t is Element of n -tuples_on BOOLEAN

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

then ex t2 being Element of T st

( t2 = t & len t2 = n ) ;

hence t is Element of n -tuples_on BOOLEAN by FINSEQ_2:92; :: thesis: verum