let F be non empty right_complementable add-associative right_zeroed distributive left_unital associative doubleLoopStr ; :: thesis: for a being Element of F

for V being non empty right_complementable add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ModuleStr over 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 vector-distributive scalar-distributive scalar-associative scalar-unital ModuleStr over 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 vector-distributive scalar-distributive scalar-associative scalar-unital ModuleStr over 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 17

.= ((1. F) + (0. F)) * v by VECTSP_1:def 15

.= (1. F) * v by RLVECT_1:4

.= v by VECTSP_1:def 17

.= v + (0. V) by RLVECT_1:4 ;

hence A1: (0. F) * v = 0. V by RLVECT_1:8; :: thesis: x * (0. V) = 0. V

hence x * (0. V) = (x * (0. F)) * v by VECTSP_1:def 16

.= 0. V by A1 ;

:: thesis: verum

for V being non empty right_complementable add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ModuleStr over 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 vector-distributive scalar-distributive scalar-associative scalar-unital ModuleStr over 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 vector-distributive scalar-distributive scalar-associative scalar-unital ModuleStr over 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 17

.= ((1. F) + (0. F)) * v by VECTSP_1:def 15

.= (1. F) * v by RLVECT_1:4

.= v by VECTSP_1:def 17

.= v + (0. V) by RLVECT_1:4 ;

hence A1: (0. F) * v = 0. V by RLVECT_1:8; :: thesis: x * (0. V) = 0. V

hence x * (0. V) = (x * (0. F)) * v by VECTSP_1:def 16

.= 0. V by A1 ;

:: thesis: verum