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 z in Seg s ; :: thesis: ex x being Element of NAT st S₁[z,x]
then reconsider z = z as non zero Nat by FINSEQ_1:1;
reconsider x = H₁(z) as Element of NAT by ORDINAL1:def 12;
take x ; :: thesis: S₁[z,x]
thus S₁[z,x] ; :: thesis: verum

end;

consider p being FinSequence of NAT such that
A2: dom p = Seg s and
A3: 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 = (k |^ ((sequenceAk1Pk s) . k)) * (Product ((idseq s) to_power (sequenceAnPk (s,k)))) ) )
s in NAT by ORDINAL1:def 12;
hence len p = s by A2, FINSEQ_1:def 3; :: thesis: for k being non zero Nat st k <= s holds
p . k = (k |^ ((sequenceAk1Pk s) . k)) * (Product ((idseq s) to_power (sequenceAnPk (s,k))))
let k be non zero Nat; :: thesis: ( k <= s implies p . k = (k |^ ((sequenceAk1Pk s) . k)) * (Product ((idseq s) to_power (sequenceAnPk (s,k)))) )
assume A4: k <= s ; :: thesis: p . k = (k |^ ((sequenceAk1Pk s) . k)) * (Product ((idseq s) to_power (sequenceAnPk (s,k))))
1 <= k by NAT_1:14;
then k in Seg s by A4;
hence p . k = (k |^ ((sequenceAk1Pk s) . k)) * (Product ((idseq s) to_power (sequenceAnPk (s,k)))) by A3, A4; :: thesis: verum