theorem Th2: :: SEQ_2:2

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