let a be non zero Real; :: thesis: for u being Element of (TOP-REAL 3) st a * u = 0. (TOP-REAL 3) holds
u is zero
let u be Element of (TOP-REAL 3); :: thesis: ( a * u = 0. (TOP-REAL 3) implies u is zero )
assume a * u = 0. (TOP-REAL 3) ; :: thesis: u is zero
then |[(a * (u `1)),(a * (u `2)),(a * (u `3))]| = |[0,0,0]| by EUCLID_5:4, EUCLID_5:7;
then ( u `1 = 0 & u `2 = 0 & u `3 = 0 ) by FINSEQ_1:78;
hence u is zero by EUCLID_5:3, EUCLID_5:4; :: thesis: verum