let f1, f2 be Function of (T -level n),NAT; :: 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

f1 . t = (Absval F) + 1 ) & ( 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

f2 . t = (Absval F) + 1 ) implies f1 = f2 )

assume that

A7: 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

f1 . t = (Absval F) + 1 and

A8: 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

f2 . t = (Absval F) + 1 ; :: thesis: f1 = f2

for F being Element of n -tuples_on BOOLEAN st F = Rev t holds

f1 . t = (Absval F) + 1 ) & ( 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

f2 . t = (Absval F) + 1 ) implies f1 = f2 )

assume that

A7: 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

f1 . t = (Absval F) + 1 and

A8: 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

f2 . t = (Absval F) + 1 ; :: thesis: f1 = f2

now :: thesis: for x being object st x in T -level n holds

f1 . x = f2 . x

hence
f1 = f2
by FUNCT_2:12; :: thesis: verumf1 . x = f2 . x

let x be object ; :: thesis: ( x in T -level n implies f1 . x = f2 . x )

assume A9: x in T -level n ; :: thesis: f1 . x = f2 . x

then x 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

A10: t = x and

A11: len t = n ;

len (Rev t) = n by A11, FINSEQ_5:def 3;

then reconsider F = Rev t as Element of n -tuples_on BOOLEAN by FINSEQ_2:92;

thus f1 . x = (Absval F) + 1 by A7, A9, A10

.= f2 . x by A8, A9, A10 ; :: thesis: verum

end;assume A9: x in T -level n ; :: thesis: f1 . x = f2 . x

then x 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

A10: t = x and

A11: len t = n ;

len (Rev t) = n by A11, FINSEQ_5:def 3;

then reconsider F = Rev t as Element of n -tuples_on BOOLEAN by FINSEQ_2:92;

thus f1 . x = (Absval F) + 1 by A7, A9, A10

.= f2 . x by A8, A9, A10 ; :: thesis: verum