let F be non empty right_complementable Abelian add-associative right_zeroed associative right_unital well-unital distributive doubleLoopStr ; :: thesis: for V being non empty right_complementable add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ModuleStr over F
for x being Element of F
for v being Element of V holds x * (- v) = - (x * 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 x being Element of F
for v being Element of V holds x * (- v) = - (x * v)
let x be Element of F; :: thesis: for v being Element of V holds x * (- v) = - (x * v)
let v be Element of V; :: thesis: x * (- v) = - (x * v)
x * (- v) = x * ((- (1. F)) * v) by Th10
.= (x * (- (1. F))) * v by Def15
.= (- (x * (1. F))) * v by Th4
.= (- x) * v ;
hence x * (- v) = - (x * v) by Th17; :: thesis: verum