:: deftheorem Def2 defines ^ RVSUM_4:def 10 :
for f being FinSequence
for g being XFinSequence
for b₃ being FinSequence holds
( b₃ = f ^ g iff ( dom b₃ = Seg ((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 ) ) );