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