defpred S₁[ object , object ] means for k being non zero Nat st k = $1 & k <= s holds
$2 = H₁(k);
A1: 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 A2: z in Seg s ; :: thesis: ex x being Element of NAT st S₁[z,x]
reconsider z = z as non zero Nat by A2, FINSEQ_1:1;
reconsider x = (((sequenceA s) . z) + 1) div (primenumber (z - 1)) as Element of NAT ;
take x ; :: thesis: S₁[z,x]
thus S₁[z,x] by Th46, RING_3:6; :: thesis: verum

end;

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