:: deftheorem Def1 defines ^ RVSUM_4:def 9 :
for f being XFinSequence
for g being FinSequence
for b₃ being XFinSequence holds
( b₃ = f ^ g iff ( dom b₃ = (len f) + (len g) & ( for k being Nat st k in dom f holds
b₃ . k = f . k ) & ( for k being Nat st k in dom g holds
b₃ . (((len f) + k) - 1) = g . k ) ) );