let A be Point of (TOP-REAL 2); :: thesis: for lambda being Real holds
( (lambda * A) `1 = lambda * (A `1) & (lambda * A) `2 = lambda * (A `2) )
let lambda be Real; :: thesis: ( (lambda * A) `1 = lambda * (A `1) & (lambda * A) `2 = lambda * (A `2) )
lambda * A = |[(lambda * (A `1)),(lambda * (A `2))]| by EUCLID:57;
hence ( (lambda * A) `1 = lambda * (A `1) & (lambda * A) `2 = lambda * (A `2) ) by EUCLID:52; :: thesis: verum