theorem Th44: :: CONVEX4:44
for a being Real
for z being Complex st 0 <= a & a <= 1 holds
( |.(a * z).| = a * |.z.| & |.((1r - a) * z).| = (1r - a) * |.z.| )