:: deftheorem defines Problem58Solution NUMBER15:def 8 :
for s being Nat holds Problem58Solution s = (numberQ s) (#) (idseq s);