theorem Th1: :: POLYNOM9:1

for i being Integer holds i '*' (1_ F_Complex) = i