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
now :: thesis: for x being object st x in T -level n holds
f1 . 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;
hence f1 = f2 by FUNCT_2:12; :: thesis: verum