let F be non empty right_complementable add-associative right_zeroed associative distributive left_unital doubleLoopStr ; :: thesis: for a being Element of F
for V being non empty right_complementable add-associative right_zeroed VectSp-like VectSpStr of F
for v being Vector of V holds
( (0. F) * v = 0. V & a * (0. V) = 0. V )
let x be Element of F; :: thesis: for V being non empty right_complementable add-associative right_zeroed VectSp-like VectSpStr of F
for v being Vector of V holds
( (0. F) * v = 0. V & x * (0. V) = 0. V )
let V be non empty right_complementable add-associative right_zeroed VectSp-like VectSpStr of F; :: thesis: for v being Vector of V holds
( (0. F) * v = 0. V & x * (0. V) = 0. V )
let v be Vector of V; :: thesis: ( (0. F) * v = 0. V & x * (0. V) = 0. V )
v + ((0. F) * v) = ((1. F) * v) + ((0. F) * v) by VECTSP_1:def 26
.= ((1. F) + (0. F)) * v by VECTSP_1:def 26
.= (1. F) * v by RLVECT_1:10
.= v by VECTSP_1:def 26
.= v + (0. V) by RLVECT_1:10 ;
hence A1: (0. F) * v = 0. V by RLVECT_1:21; :: thesis: x * (0. V) = 0. V
hence x * (0. V) = (x * (0. F)) * v by VECTSP_1:def 26
.= 0. V by A1, VECTSP_1:36 ;
:: thesis: verum