let k, s be Nat; :: thesis: ( 1 <= k & k <= s implies (Problem58Solution s) . k = k * (numberQ s) )
assume ( 1 <= k & k <= s ) ; :: thesis: (Problem58Solution s) . k = k * (numberQ s)
then k in Seg s ;
hence k * (numberQ s) = (numberQ s) * ((idseq s) . k) by FINSEQ_2:49
.= (Problem58Solution s) . k by VALUED_1:6 ;
:: thesis: verum