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, w being Element of V holds x * (v - w) = (x * v) - (x * w)
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, w being Element of V holds x * (v - w) = (x * v) - (x * w)
let x be Element of F; :: thesis: for v, w being Element of V holds x * (v - w) = (x * v) - (x * w)
let v, w be Element of V; :: thesis: x * (v - w) = (x * v) - (x * w)
x * (v - w) = (x * v) + (x * (- w)) by Def13
.= (x * v) + (- (x * w)) by Th18 ;
hence x * (v - w) = (x * v) - (x * w) ; :: thesis: verum