let F1, F2 be FinSequence of PFuncs ((ND (V,A)),(ND (V,A))); ( len F1 = len val & ( for n being Nat st 1 <= n & n <= len F1 holds
F1 . n = denaming (V,A,(val . n)) ) & len F2 = len val & ( for n being Nat st 1 <= n & n <= len F2 holds
F2 . n = denaming (V,A,(val . n)) ) implies F1 = F2 )
assume that
A4:
len F1 = len val
and
A5:
for n being Nat st 1 <= n & n <= len F1 holds
F1 . n = denaming (V,A,(val . n))
and
A6:
len F2 = len val
and
A7:
for n being Nat st 1 <= n & n <= len F2 holds
F2 . n = denaming (V,A,(val . n))
; F1 = F2
for n being Nat st 1 <= n & n <= len val holds
F1 . n = F2 . n
hence
F1 = F2
by A4, A6, FINSEQ_1:def 17; verum