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)) )