theorem Th48: :: NUMBER15:48
for k, s being Nat st 1 <= k & k <= s holds
(Problem58Solution s) . k = k * (numberQ s)