theorem Th8: :: POLYNOM5:8

|.(<*> the carrier of F_Complex).| = <*> REAL