theorem Th34: :: COMPLSP2:41

for x being FinSequence of COMPLEX
for c being Complex holds c * (0c (len x)) = 0c (len x)