let a be Real; :: thesis: for p, q, r being Point of (TOP-REAL 3) holds |{(a * p),q,r}| = a * |{p,q,r}|
let p, q, r be Point of (TOP-REAL 3); :: thesis: |{(a * p),q,r}| = a * |{p,q,r}|
|{(a * p),q,r}| = ((((((((a * p) `1) * (q `2)) * (r `3)) - ((((a * p) `3) * (q `2)) * (r `1))) - ((((a * p) `1) * (q `3)) * (r `2))) + ((((a * p) `2) * (q `3)) * (r `1))) - ((((a * p) `2) * (q `1)) * (r `3))) + ((((a * p) `3) * (q `1)) * (r `2)) by Th23
.= (((((((a * (p `1)) * (q `2)) * (r `3)) - ((((a * p) `3) * (q `2)) * (r `1))) - ((((a * p) `1) * (q `3)) * (r `2))) + ((((a * p) `2) * (q `3)) * (r `1))) - ((((a * p) `2) * (q `1)) * (r `3))) + ((((a * p) `3) * (q `1)) * (r `2)) by EUCLID_5:9
.= (((((((a * (p `1)) * (q `2)) * (r `3)) - (((a * (p `3)) * (q `2)) * (r `1))) - ((((a * p) `1) * (q `3)) * (r `2))) + ((((a * p) `2) * (q `3)) * (r `1))) - ((((a * p) `2) * (q `1)) * (r `3))) + ((((a * p) `3) * (q `1)) * (r `2)) by EUCLID_5:9
.= (((((((a * (p `1)) * (q `2)) * (r `3)) - (((a * (p `3)) * (q `2)) * (r `1))) - (((a * (p `1)) * (q `3)) * (r `2))) + ((((a * p) `2) * (q `3)) * (r `1))) - ((((a * p) `2) * (q `1)) * (r `3))) + ((((a * p) `3) * (q `1)) * (r `2)) by EUCLID_5:9
.= (((((((a * (p `1)) * (q `2)) * (r `3)) - (((a * (p `3)) * (q `2)) * (r `1))) - (((a * (p `1)) * (q `3)) * (r `2))) + (((a * (p `2)) * (q `3)) * (r `1))) - ((((a * p) `2) * (q `1)) * (r `3))) + ((((a * p) `3) * (q `1)) * (r `2)) by EUCLID_5:9
.= (((((((a * (p `1)) * (q `2)) * (r `3)) - (((a * (p `3)) * (q `2)) * (r `1))) - (((a * (p `1)) * (q `3)) * (r `2))) + (((a * (p `2)) * (q `3)) * (r `1))) - (((a * (p `2)) * (q `1)) * (r `3))) + ((((a * p) `3) * (q `1)) * (r `2)) by EUCLID_5:9
.= (((((((a * (p `1)) * (q `2)) * (r `3)) - (((a * (p `3)) * (q `2)) * (r `1))) - (((a * (p `1)) * (q `3)) * (r `2))) + (((a * (p `2)) * (q `3)) * (r `1))) - (((a * (p `2)) * (q `1)) * (r `3))) + (((a * (p `3)) * (q `1)) * (r `2)) by EUCLID_5:9
.= a * ((((((((p `1) * (q `2)) * (r `3)) - (((p `3) * (q `2)) * (r `1))) - (((p `1) * (q `3)) * (r `2))) + (((p `2) * (q `3)) * (r `1))) - (((p `2) * (q `1)) * (r `3))) + (((p `3) * (q `1)) * (r `2)))
.= a * |{p,q,r}| by Th23 ;
hence |{(a * p),q,r}| = a * |{p,q,r}| ; :: thesis: verum