let a be real number ; :: thesis: for V being RealLinearSpace
for v being VECTOR of V st ( a = 0 or v = 0. V ) holds
a * v = 0. V
let V be RealLinearSpace; :: thesis: for v being VECTOR of V st ( a = 0 or v = 0. V ) holds
a * v = 0. V
let v be VECTOR of V; :: thesis: ( ( a = 0 or v = 0. V ) implies a * v = 0. V )
assume A1: ( a = 0 or v = 0. V ) ; :: thesis: a * v = 0. V

now

per cases ( a = 0 or v = 0. V ) by A1;

suppose A2: a = 0 ; :: thesis: a * v = 0. V

v + (0 * v) = (1 * v) + (0 * v) by Def11
.= (1 + 0 ) * v by Def9
.= v by Def11
.= v + (0. V) by Th10 ;
hence a * v = 0. V by A2, Th21; :: thesis: verum

end;

suppose A3: v = 0. V ; :: thesis: a * v = 0. V

(a * (0. V)) + (a * (0. V)) = a * ((0. V) + (0. V)) by Def8
.= a * (0. V) by Th10
.= (a * (0. V)) + (0. V) by Th10 ;
hence a * v = 0. V by A3, Th21; :: thesis: verum

end;

end;

end;

hence a * v = 0. V ; :: thesis: verum