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 VectSpStr of 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 VectSpStr of 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 Th59
.= (x * (- (1. F))) * v by Def28
.= (- (x * (1. F))) * v by Th40
.= (- x) * v by Def13 ;
hence x * (- v) = - (x * v) by Th68; :: thesis: verum