let F1, F2 be FinSequence of PFuncs ((ND (V,A)),(ND (V,A))); :: thesis: ( 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)) ; :: thesis: F1 = F2
for n being Nat st 1 <= n & n <= len val holds
F1 . n = F2 . n
proof
let n be Nat; :: thesis: ( 1 <= n & n <= len val implies F1 . n = F2 . n )
assume A8: ( 1 <= n & n <= len val ) ; :: thesis: F1 . n = F2 . n
hence F1 . n = denaming (V,A,(val . n)) by A4, A5
.= F2 . n by A6, A7, A8 ;
:: thesis: verum
end;
hence F1 = F2 by A4, A6, FINSEQ_1:def 17; :: thesis: verum