let f, g, h, k be real-valued FinSequence; :: thesis: (f + g) - (h + k) = (f - h) + (g - k)
thus (f + g) - (h + k) = f + (g + (- (h + k))) by RVSUM_1:15
.= f + (g + ((- h) + (- k))) by RVSUM_1:26
.= f + ((- h) + (g + (- k))) by RVSUM_1:15
.= (f + (- h)) + (g + (- k)) by RVSUM_1:15
.= (f - h) + (g + (- k))
.= (f - h) + (g - k) ; :: thesis: verum