let f, g be FinSequence of NAT ; :: thesis: ( len f = s & ( for k being non zero Nat st k <= s holds
f . k = (k |^ ((sequenceAk1Pk s) . k)) * (Product ((idseq s) to_power (sequenceAnPk (s,k)))) ) & len g = s & ( for k being non zero Nat st k <= s holds
g . k = (k |^ ((sequenceAk1Pk s) . k)) * (Product ((idseq s) to_power (sequenceAnPk (s,k)))) ) implies f = g )
assume that
A5: len f = s and
A6: for k being non zero Nat st k <= s holds
f . k = H₁(k) and
A7: len g = s and
A8: for k being non zero Nat st k <= s holds
g . k = H₁(k) ; :: thesis: f = g
thus len f = len g by A5, A7; :: according to FINSEQ_1:def 18 :: thesis: for b₁ being set holds
( not 1 <= b₁ or not b₁ <= len f or f . b₁ = g . b₁ )
let k be Nat; :: thesis: ( not 1 <= k or not k <= len f or f . k = g . k )
assume that
A9: 1 <= k and
A10: k <= len f ; :: thesis: f . k = g . k
reconsider k = k as non zero Nat by A9;
f . k = H₁(k) by A5, A6, A10
.= g . k by A5, A8, A10 ;
hence f . k = g . k ; :: thesis: verum