:: deftheorem defines ^ RVSUM_4:def 4 :
for f being complex-valued XFinSequence
for seq being Complex_Sequence holds f ^ seq = f \/ (Shift (seq,(len f)));