let a be Real; :: thesis: for V being non empty right_complementable add-associative right_zeroed vector-distributive scalar-distributive scalar-unital RLSStruct
for v being Element of V st ( a = 0 or v = 0. V ) holds
a * v = 0. V
let V be non empty right_complementable add-associative right_zeroed vector-distributive scalar-distributive scalar-unital RLSStruct ; :: thesis: for v being Element of V st ( a = 0 or v = 0. V ) holds
a * v = 0. V
let v be Element of V; :: thesis: ( ( a = 0 or v = 0. V ) implies a * v = 0. V )
assume ( a = 0 or v = 0. V ) ; :: thesis: a * v = 0. V
per cases then ( a = 0 or v = 0. V ) ;
suppose A1: a = 0 ; :: thesis: a * v = 0. V
v + (0 * v) = (1 * v) + (0 * v) by Def8
.= (1 + 0) * v by Def6
.= v + (0. V) by Def8 ;
hence a * v = 0. V by A1, Th8; :: thesis: verum
end;
suppose A2: v = 0. V ; :: thesis: a * v = 0. V
(a * (0. V)) + (a * (0. V)) = a * ((0. V) + (0. V)) by Def5
.= (a * (0. V)) + (0. V) ;
hence a * v = 0. V by A2, Th8; :: thesis: verum
end;
end;