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