defpred S₁[ 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 = (Absval F) + 1 ) );
A1: for e being object st e in T -level n holds
ex u being object st
( u in NAT & S₁[e,u] )

let e be object ; :: thesis:
assume e in T -level n ; :: thesis:
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 A3, FINSEQ_5:def 3;
then reconsider F1 = Rev t as Element of n -tuples_on BOOLEAN by FINSEQ_2:92;
take u = (Absval F1) + 1; :: thesis:
thus u in NAT ; :: thesis:
take t ; :: thesis:
thus t = e by A2; :: thesis:
let F be Tuple of n, BOOLEAN ; :: thesis:
assume F = Rev t ; :: thesis:
hence u = (Absval F) + 1 ; :: thesis:

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
S₁[e,f . e] from FUNCT_1:sch 6(A1);
reconsider f = f as Function of (T -level n),NAT by A4, FUNCT_2:2;
take f ; :: thesis:
let t be Element of T; :: thesis:
assume t in T -level n ; :: thesis:
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 = (Absval F) + 1 ) ) by A5;
let F be Element of n -tuples_on BOOLEAN; :: thesis:
assume F = Rev t ; :: thesis:
hence f . t = (Absval F) + 1 by A6; :: thesis: