let a be Real; 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); |{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}|
; verum