for n being Nat
for cF being complex-valued XFinSequence
for c being Complex holds c (#) (cF | n) = (c (#) cF) | n