let R be non empty right_complementable right_unital well-unital distributive Abelian add-associative right_zeroed associative doubleLoopStr ; :: thesis: for V being non empty right_complementable add-associative right_zeroed RightMod-like RightModStr over R
for x being Scalar of R
for v, w being Vector of V holds (v - w) * x = (v * x) - (w * x)
let V be non empty right_complementable add-associative right_zeroed RightMod-like RightModStr over R; :: thesis: for x being Scalar of R
for v, w being Vector of V holds (v - w) * x = (v * x) - (w * x)
let x be Scalar of R; :: thesis: for v, w being Vector of V holds (v - w) * x = (v * x) - (w * x)
let v, w be Vector of V; :: thesis: (v - w) * x = (v * x) - (w * x)
(v - w) * x = (v + (- w)) * x
.= (v * x) + ((- w) * x) by Def8
.= (v * x) + (- (w * x)) by Th34 ;
hence (v - w) * x = (v * x) - (w * x) ; :: thesis: verum