let a1, a2, a3, b1, b2, b3 be Real; :: thesis: for n being Element of NAT
for x1, x2, x3 being Element of REAL n holds (((a1 * x1) + (a2 * x2)) + (a3 * x3)) - (((b1 * x1) + (b2 * x2)) + (b3 * x3)) = (((a1 - b1) * x1) + ((a2 - b2) * x2)) + ((a3 - b3) * x3)
let n be Element of NAT ; :: thesis: for x1, x2, x3 being Element of REAL n holds (((a1 * x1) + (a2 * x2)) + (a3 * x3)) - (((b1 * x1) + (b2 * x2)) + (b3 * x3)) = (((a1 - b1) * x1) + ((a2 - b2) * x2)) + ((a3 - b3) * x3)
let x1, x2, x3 be Element of REAL n; :: thesis: (((a1 * x1) + (a2 * x2)) + (a3 * x3)) - (((b1 * x1) + (b2 * x2)) + (b3 * x3)) = (((a1 - b1) * x1) + ((a2 - b2) * x2)) + ((a3 - b3) * x3)
thus (((a1 * x1) + (a2 * x2)) + (a3 * x3)) - (((b1 * x1) + (b2 * x2)) + (b3 * x3)) = (((a1 * x1) + (a2 * x2)) - ((b1 * x1) + (b2 * x2))) + ((a3 * x3) - (b3 * x3)) by Th23
.= (((a1 - b1) * x1) + ((a2 - b2) * x2)) + ((a3 * x3) - (b3 * x3)) by Th30
.= (((a1 - b1) * x1) + ((a2 - b2) * x2)) + ((a3 - b3) * x3) by Th16 ; :: thesis: verum