let x be Element of INT.Ring; :: thesis: for V being non empty right_complementable add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ModuleStr over INT.Ring
for v being Vector of V holds
( (0. INT.Ring) * 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 INT.Ring ; :: thesis: for v being Vector of V holds
( (0. INT.Ring) * v = 0. V & x * (0. V) = 0. V )
let v be Vector of V; :: thesis: ( (0. INT.Ring) * v = 0. V & x * (0. V) = 0. V )
A1: v + ((0. INT.Ring) * v) = ((1. INT.Ring) * v) + ((0. INT.Ring) * v) by VECTSP_1:def 17
.= ((1. INT.Ring) + (0. INT.Ring)) * v by VECTSP_1:def 15
.= v + (0. V) by VECTSP_1:def 17 ;
hence (0. INT.Ring) * v = 0. V by RLVECT_1:8; :: thesis: x * (0. V) = 0. V
hence x * (0. V) = (x * (0. INT.Ring)) * v by VECTSP_1:def 16
.= 0. V by A1, RLVECT_1:8 ;
:: thesis: verum