let a be Real; :: thesis: for V being non empty right_complementable add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct
for v being Element of V holds
( not a * v = 0. V or a = 0 or v = 0. V )
let V be non empty right_complementable add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct ; :: thesis: for v being Element of V holds
( not a * v = 0. V or a = 0 or v = 0. V )
let v be Element of V; :: thesis: ( not a * v = 0. V or a = 0 or v = 0. V )
assume that
A1: a * v = 0. V and
A2: a <> 0 ; :: thesis: v = 0. V
thus v = 1 * v by Def8
.= ((a ") * a) * v by A2, XCMPLX_0:def 7
.= (a ") * (0. V) by A1, Def7
.= 0. V ; :: thesis: verum