theorem Th2: :: MENELAUS:2
for A being Point of (TOP-REAL 2)
for lambda being Real holds
( (lambda * A) `1 = lambda * (A `1) & (lambda * A) `2 = lambda * (A `2) )