set f = Problem58Solution s;
A1: len (Problem58Solution s) = s by CARD_1:def 7;
let i be Nat; :: according to NUMBER06:def 3 :: thesis: ( not i in dom (Problem58Solution s) or not i + 1 in dom (Problem58Solution s) or not i + 2 in dom (Problem58Solution s) or ((Problem58Solution s) . (i + 2)) - ((Problem58Solution s) . (i + 1)) = ((Problem58Solution s) . (i + 1)) - ((Problem58Solution s) . i) )
assume i in dom (Problem58Solution s) ; :: thesis: ( not i + 1 in dom (Problem58Solution s) or not i + 2 in dom (Problem58Solution s) or ((Problem58Solution s) . (i + 2)) - ((Problem58Solution s) . (i + 1)) = ((Problem58Solution s) . (i + 1)) - ((Problem58Solution s) . i) )
then ( 1 <= i & i <= s ) by A1, FINSEQ_3:25;
then A2: (Problem58Solution s) . i = i * (numberQ s) by Th48;
assume i + 1 in dom (Problem58Solution s) ; :: thesis: ( not i + 2 in dom (Problem58Solution s) or ((Problem58Solution s) . (i + 2)) - ((Problem58Solution s) . (i + 1)) = ((Problem58Solution s) . (i + 1)) - ((Problem58Solution s) . i) )
then ( 1 <= i + 1 & i + 1 <= s ) by A1, FINSEQ_3:25;
then A3: (Problem58Solution s) . (i + 1) = (i + 1) * (numberQ s) by Th48;
assume i + 2 in dom (Problem58Solution s) ; :: thesis: ((Problem58Solution s) . (i + 2)) - ((Problem58Solution s) . (i + 1)) = ((Problem58Solution s) . (i + 1)) - ((Problem58Solution s) . i)
then ( 1 <= i + 2 & i + 2 <= s ) by A1, FINSEQ_3:25;
then (Problem58Solution s) . (i + 2) = (i + 2) * (numberQ s) by Th48;
hence ((Problem58Solution s) . (i + 2)) - ((Problem58Solution s) . (i + 1)) = ((Problem58Solution s) . (i + 1)) - ((Problem58Solution s) . i) by A2, A3; :: thesis: verum