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] )

proof

let e be object ; :: thesis: ( e in T -level n implies ex u being object st
( u in NAT & S₁[e,u] ) )
assume e in T -level n ; :: thesis: ex u being object st
( u in NAT & S₁[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 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: ( u in NAT & S₁[e,u] )
thus u in NAT ; :: thesis: S₁[e,u]
take t ; :: thesis: ( t = e & ( for F being Tuple of n, BOOLEAN st F = Rev t holds
u = (Absval F) + 1 ) )
thus t = e by A2; :: thesis: for F being Tuple of n, BOOLEAN st F = Rev t holds
u = (Absval F) + 1
let F be Tuple of n, BOOLEAN ; :: thesis: ( F = Rev t implies u = (Absval F) + 1 )
assume F = Rev t ; :: thesis: u = (Absval F) + 1
hence u = (Absval F) + 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
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: 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 = (Absval F) + 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 = (Absval F) + 1 )
assume t in T -level n ; :: thesis: for F being Element of n -tuples_on BOOLEAN st F = Rev t holds
f . t = (Absval F) + 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 = (Absval F) + 1 ) ) by A5;
let F be Element of n -tuples_on BOOLEAN; :: thesis: ( F = Rev t implies f . t = (Absval F) + 1 )
assume F = Rev t ; :: thesis: f . t = (Absval F) + 1
hence f . t = (Absval F) + 1 by A6; :: thesis: verum