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