defpred S1[ object , object ] means ex t being Element of T st
( t = \$1 & ( for F being Tuple of n, BOOLEAN st F = Rev t holds
\$2 = () + 1 ) );
A1: for e being object st e in T -level n holds
ex u being object st
( u in NAT & S1[e,u] )
proof
let e be object ; :: thesis: ( e in T -level n implies ex u being object st
( u in NAT & S1[e,u] ) )

assume e in T -level n ; :: thesis: ex u being object st
( u in NAT & S1[e,u] )

then e in { w where w is Element of T : len w = n } by TREES_2:def 6;
then consider t being Element of T such that
A2: t = e and
A3: len t = n ;
len (Rev t) = n by ;
then reconsider F1 = Rev t as Element of n -tuples_on BOOLEAN by FINSEQ_2:92;
take u = (Absval F1) + 1; :: thesis: ( u in NAT & S1[e,u] )
thus u in NAT ; :: thesis: S1[e,u]
take t ; :: thesis: ( t = e & ( for F being Tuple of n, BOOLEAN st F = Rev t holds
u = () + 1 ) )

thus t = e by A2; :: thesis: for F being Tuple of n, BOOLEAN st F = Rev t holds
u = () + 1

let F be Tuple of n, BOOLEAN ; :: thesis: ( F = Rev t implies u = () + 1 )
assume F = Rev t ; :: thesis: u = () + 1
hence u = () + 1 ; :: thesis: verum
end;
consider f being Function such that
A4: ( dom f = T -level n & rng f c= NAT ) and
A5: for e being object st e in T -level n holds
S1[e,f . e] from reconsider f = f as Function of (T -level n),NAT by ;
take f ; :: thesis: for t being Element of T st t in T -level n holds
for F being Element of n -tuples_on BOOLEAN st F = Rev t holds
f . t = () + 1

let t be Element of T; :: thesis: ( t in T -level n implies for F being Element of n -tuples_on BOOLEAN st F = Rev t holds
f . t = () + 1 )

assume t in T -level n ; :: thesis: for F being Element of n -tuples_on BOOLEAN st F = Rev t holds
f . t = () + 1

then A6: ex t1 being Element of T st
( t1 = t & ( for F being Tuple of n, BOOLEAN st F = Rev t1 holds
f . t = () + 1 ) ) by A5;
let F be Element of n -tuples_on BOOLEAN; :: thesis: ( F = Rev t implies f . t = () + 1 )
assume F = Rev t ; :: thesis: f . t = () + 1
hence f . t = () + 1 by A6; :: thesis: verum