:: deftheorem Def4 defines GoCross_Seq_REAL FINANCE2:def 2 :
for k being Nat
for pm being Element of REAL
for b₃ being SetSequence of REAL holds
( b₃ = GoCross_Seq_REAL (pm,k) iff for n being Nat holds b₃ . n = {((pm * k) * ((n + 1) "))} );