let V be RealLinearSpace; :: thesis: for p, q being Element of V
for a being Real st a * p = q & a <> 0 & not p is zero holds
not q is zero
let p, q be Element of V; :: thesis: for a being Real st a * p = q & a <> 0 & not p is zero holds
not q is zero
let a be Real; :: thesis: ( a * p = q & a <> 0 & not p is zero implies not q is zero )
assume A1: ( a * p = q & a <> 0 & not p is zero ) ; :: thesis: not q is zero
then p <> 0. V by STRUCT_0:def 15;
then q <> 0. V by A1, RLVECT_1:24;
hence not q is zero by STRUCT_0:def 15; :: thesis: verum