let a1, a2, a3 be Real; :: thesis: 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))
let n be Nat; :: thesis: 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))
let x, x1, x2, x3 be Element of REAL n; :: thesis: x - (((a1 * x1) + (a2 * x2)) + (a3 * x3)) = x + ((((- a1) * x1) + ((- a2) * x2)) + ((- a3) * x3))
thus x - (((a1 * x1) + (a2 * x2)) + (a3 * x3)) = x + (((- (a1 * x1)) + (- (a2 * x2))) + (- (a3 * x3))) by Th8
.= x + ((((- a1) * x1) + (- (a2 * x2))) + (- (a3 * x3))) by Th3
.= x + ((((- a1) * x1) + ((- a2) * x2)) + (- (a3 * x3))) by Th3
.= x + ((((- a1) * x1) + ((- a2) * x2)) + ((- a3) * x3)) by Th3 ; :: thesis: verum