let a be Real; :: thesis: for p, q, r being Point of (TOP-REAL 3) holds |{p,(a * q),r}| = a * |{p,q,r}|
let p, q, r be Point of (TOP-REAL 3); :: thesis: |{p,(a * q),r}| = a * |{p,q,r}|
|{p,(a * q),r}| = - |{(a * q),p,r}| by Th25
.= - (a * |{q,p,r}|) by Th26
.= - (a * (- |{p,q,r}|)) by Th25 ;
hence |{p,(a * q),r}| = a * |{p,q,r}| ; :: thesis: verum