defpred S_{1}[ 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_{1}[e,u] )

A4: ( dom f = T -level n & rng f c= NAT ) and

A5: for e being object st e in T -level n holds

S_{1}[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

( 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

proof

consider f being Function such that
let e be object ; :: thesis: ( e in T -level n implies ex u being object st

( u in NAT & S_{1}[e,u] ) )

assume e in T -level n ; :: thesis: ex u being object st

( u in NAT & S_{1}[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_{1}[e,u] )

thus u in NAT ; :: thesis: S_{1}[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;( u in NAT & S

assume e in T -level n ; :: thesis: ex u being object st

( u in NAT & S

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

thus u in NAT ; :: thesis: S

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

A4: ( dom f = T -level n & rng f c= NAT ) and

A5: for e being object st e in T -level n holds

S

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