theorem Th1: :: COMSEQ_2:1

for r, g being Complex st g <> 0c & r <> 0c holds
|.((g ") - (r ")).| = |.(g - r).| / (|.g.| * |.r.|)