for seq being Complex_Sequence
for r being Real holds
( r (#) (Re seq) = Re (r (#) seq) & r (#) (Im seq) = Im (r (#) seq) )