let f, g be FinSequence of NAT ; :: thesis: ( len f = s & ( for n being non zero Nat st n <= s holds
( ( n <> k implies f . n = ((sequenceA s) . n) / (primenumber (k - 1)) ) & ( n = k implies f . n = 0 ) ) ) & len g = s & ( for n being non zero Nat st n <= s holds
( ( n <> k implies g . n = ((sequenceA s) . n) / (primenumber (k - 1)) ) & ( n = k implies g . n = 0 ) ) ) implies f = g )
assume that
A9: len f = s and
A10: for z being non zero Nat st z <= s holds
( ( z <> k implies f . z = H₁(z) ) & ( z = k implies f . z = 0 ) ) and
A11: len g = s and
A12: for z being non zero Nat st z <= s holds
( ( z <> k implies g . z = H₁(z) ) & ( z = k implies g . z = 0 ) ) ; :: thesis: f = g
thus len f = len g by A9, A11; :: 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 z be Nat; :: thesis: ( not 1 <= z or not z <= len f or f . z = g . z )
assume that
A13: 1 <= z and
A14: z <= len f ; :: thesis: f . z = g . z
reconsider z = z as non zero Nat by A13;

per cases ( z <> k or z = k ) ;

suppose A15: z <> k ; :: thesis: f . z = g . z

then f . z = ((sequenceA s) . z) / (primenumber (k - 1)) by A9, A10, A14
.= g . z by A9, A12, A14, A15 ;
hence f . z = g . z ; :: thesis: verum

end;

suppose A16: z = k ; :: thesis: f . z = g . z

then f . z = 0 by A9, A10, A14
.= g . z by A9, A12, A14, A16 ;
hence f . z = g . z ; :: thesis: verum

end;

end;