let p be Point of (TOP-REAL 2); :: thesis: for r being Real holds

( (r * p) `1 = r * (p `1) & (r * p) `2 = r * (p `2) )

let r be Real; :: thesis: ( (r * p) `1 = r * (p `1) & (r * p) `2 = r * (p `2) )

r * p = |[(r * (p `1)),(r * (p `2))]| by EUCLID:57;

hence ( (r * p) `1 = r * (p `1) & (r * p) `2 = r * (p `2) ) by EUCLID:52; :: thesis: verum

( (r * p) `1 = r * (p `1) & (r * p) `2 = r * (p `2) )

let r be Real; :: thesis: ( (r * p) `1 = r * (p `1) & (r * p) `2 = r * (p `2) )

r * p = |[(r * (p `1)),(r * (p `2))]| by EUCLID:57;

hence ( (r * p) `1 = r * (p `1) & (r * p) `2 = r * (p `2) ) by EUCLID:52; :: thesis: verum