theorem :: CSSPACE2:12

for seq being Complex_Sequence
for n being Nat holds
( (Re (seq (#) (seq *'))) . n >= 0 & (Im (seq (#) (seq *'))) . n = 0 ) by Lm8;