let M be non empty set ; :: thesis: for V being ComplexNormSpace
for f1, f2 being PartFunc of M,V holds f1 - (- f2) = f1 + f2
let V be ComplexNormSpace; :: thesis: for f1, f2 being PartFunc of M,V holds f1 - (- f2) = f1 + f2
let f1, f2 be PartFunc of M,V; :: thesis: f1 - (- f2) = f1 + f2
thus f1 - (- f2) = f1 + (- (- f2)) by Th25
.= f1 + f2 by Th24 ; :: thesis: verum