defpred S₁[ object , object ] means for a being non zero Nat st a = $1 & a <= s holds
( ( a <> k implies $2 = H₁(a) ) & ( a = k implies $2 = 0 ) );
A2: for z being Nat st z in Seg s holds
ex x being Element of NAT st S₁[z,x]

proof

let z be Nat; :: thesis: ( z in Seg s implies ex x being Element of NAT st S₁[z,x] )
assume A3: z in Seg s ; :: thesis: ex x being Element of NAT st S₁[z,x]
reconsider z = z as non zero Nat by A3, FINSEQ_1:1;

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

suppose A4: z <> k ; :: thesis: ex x being Element of NAT st S₁[z,x]

z <= s by A3, FINSEQ_1:1;
then ((sequenceA s) . z) / (primenumber (k - 1)) = ((sequenceA s) . z) div (primenumber (k - 1)) by A1, A4, Th47, RING_3:6;
then reconsider x = H₁(z) as Element of NAT ;
take x ; :: thesis: S₁[z,x]
thus S₁[z,x] by A4; :: thesis: verum

end;

suppose A5: z = k ; :: thesis: ex x being Element of NAT st S₁[z,x]

take 0 ; :: thesis: S₁[z, 0 ]
thus S₁[z, 0 ] by A5; :: thesis: verum

end;

end;

end;

consider p being FinSequence of NAT such that
A6: dom p = Seg s and
A7: for a being Nat st a in Seg s holds
S₁[a,p . a] from FINSEQ_1:sch 5(A2);
take p ; :: thesis: ( len p = s & ( for n being non zero Nat st n <= s holds
( ( n <> k implies p . n = ((sequenceA s) . n) / (primenumber (k - 1)) ) & ( n = k implies p . n = 0 ) ) ) )
s in NAT by ORDINAL1:def 12;
hence len p = s by A6, FINSEQ_1:def 3; :: thesis: for n being non zero Nat st n <= s holds
( ( n <> k implies p . n = ((sequenceA s) . n) / (primenumber (k - 1)) ) & ( n = k implies p . n = 0 ) )
let a be non zero Nat; :: thesis: ( a <= s implies ( ( a <> k implies p . a = ((sequenceA s) . a) / (primenumber (k - 1)) ) & ( a = k implies p . a = 0 ) ) )
assume A8: a <= s ; :: thesis: ( ( a <> k implies p . a = ((sequenceA s) . a) / (primenumber (k - 1)) ) & ( a = k implies p . a = 0 ) )
1 <= a by NAT_1:14;
then a in Seg s by A8;
hence ( ( a <> k implies p . a = ((sequenceA s) . a) / (primenumber (k - 1)) ) & ( a = k implies p . a = 0 ) ) by A7, A8; :: thesis: verum