:: deftheorem Def11 defines sequenceQk NUMBER15:def 11 :
for s being Nat
for b₂ being FinSequence of NAT holds
( b₂ = sequenceQk s iff ( len b₂ = s & ( for k being non zero Nat st k <= s holds
b₂ . k = (k |^ ((sequenceAk1Pk s) . k)) * (Product ((idseq s) to_power (sequenceAnPk (s,k)))) ) ) );