let a be Real; :: thesis: for u being Element of (TOP-REAL 3) holds (a * u) + ((- a) * u) = 0. (TOP-REAL 3)
let u be Element of (TOP-REAL 3); :: thesis: (a * u) + ((- a) * u) = 0. (TOP-REAL 3)
a * u = |[(a * (u `1)),(a * (u `2)),(a * (u `3))]| by EUCLID_5:7;
then (a * u) + ((- a) * u) = |[(a * (u `1)),(a * (u `2)),(a * (u `3))]| + |[((- a) * (u `1)),((- a) * (u `2)),((- a) * (u `3))]| by EUCLID_5:7
.= |[((a * (u `1)) + ((- a) * (u `1))),((a * (u `2)) + ((- a) * (u `2))),((a * (u `3)) + ((- a) * (u `3)))]| by EUCLID_5:6
.= |[0,0,0]| ;
hence (a * u) + ((- a) * u) = 0. (TOP-REAL 3) by EUCLID_5:4; :: thesis: verum