theorem Th14: :: EUCLIDLP:14

for a1, a2, a3 being Real
for n being Nat
for x, x1, x2, x3 being Element of REAL n holds x - (((a1 * x1) + (a2 * x2)) + (a3 * x3)) = x + ((((- a1) * x1) + ((- a2) * x2)) + ((- a3) * x3))