theorem Th9: :: TOPALG_1:9

for f, g, h, k being real-valued FinSequence holds (f + g) - (h + k) = (f - h) + (g - k)