let a be Real; :: thesis: for V being non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct
for v, w being Element of V holds a * (v - w) = (a * v) - (a * w)
let V be non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct ; :: thesis: for v, w being Element of V holds a * (v - w) = (a * v) - (a * w)
let v, w be Element of V; :: thesis: a * (v - w) = (a * v) - (a * w)
thus a * (v - w) = (a * v) + (a * (- w)) by Def5
.= (a * v) - (a * w) by Th25 ; :: thesis: verum