theorem RSH: :: RVSUM_4:62
for f being complex-valued Sequence
for n being Nat holds
( Re (Shift (f,n)) = Shift ((Re f),n) & Im (Shift (f,n)) = Shift ((Im f),n) )