let F1, F2 be complex-valued FinSequence; :: thesis: - (F1 - F2) = (- F1) + F2
thus - (F1 - F2) = (- F1) + (- (- F2)) by Th10
.= (- F1) + F2 ; :: thesis: verum