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