let C be non empty set ; :: thesis: for V being non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct
for f1, f2 being PartFunc of C,V holds f1 - (- f2) = f1 + f2
let V be non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct ; :: thesis: for f1, f2 being PartFunc of C,V holds f1 - (- f2) = f1 + f2
let f1, f2 be PartFunc of C,V; :: thesis: f1 - (- f2) = f1 + f2
thus f1 - (- f2) = f1 + (- (- f2)) by Th25
.= f1 + f2 by Th24 ; :: thesis: verum