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