:: deftheorem defines numberQ NUMBER15:def 7 :
for s being Nat holds numberQ s = Product ((idseq s) to_power (sequenceA s));