let a1, a2, b1, b2 be Real; :: thesis: for n being Nat
for x1, x2 being Element of REAL n holds ((a1 * x1) + (a2 * x2)) - ((b1 * x1) + (b2 * x2)) = ((a1 - b1) * x1) + ((a2 - b2) * x2)
let n be Nat; :: thesis: for x1, x2 being Element of REAL n holds ((a1 * x1) + (a2 * x2)) - ((b1 * x1) + (b2 * x2)) = ((a1 - b1) * x1) + ((a2 - b2) * x2)
let x1, x2 be Element of REAL n; :: thesis: ((a1 * x1) + (a2 * x2)) - ((b1 * x1) + (b2 * x2)) = ((a1 - b1) * x1) + ((a2 - b2) * x2)
thus ((a1 * x1) + (a2 * x2)) - ((b1 * x1) + (b2 * x2)) = ((a1 * x1) - (b1 * x1)) + ((a2 * x2) - (b2 * x2)) by Th18
.= ((a1 - b1) * x1) + ((a2 * x2) - (b2 * x2)) by Th11
.= ((a1 - b1) * x1) + ((a2 - b2) * x2) by Th11 ; :: thesis: verum