theorem Th99: :: RVSUM_1:99

for r1, r2 being Complex holds Product <*r1,r2*> = r1 * r2