let a, b be Real; :: thesis: for n being Nat
for x being Element of REAL n holds
( (a - b) * x = (a * x) + ((- b) * x) & (a - b) * x = (a * x) + (- (b * x)) & (a - b) * x = (a * x) - (b * x) )
let n be Nat; :: thesis: for x being Element of REAL n holds
( (a - b) * x = (a * x) + ((- b) * x) & (a - b) * x = (a * x) + (- (b * x)) & (a - b) * x = (a * x) - (b * x) )
let x be Element of REAL n; :: thesis: ( (a - b) * x = (a * x) + ((- b) * x) & (a - b) * x = (a * x) + (- (b * x)) & (a - b) * x = (a * x) - (b * x) )
thus A1: (a - b) * x = (a + (- b)) * x
.= (a * x) + ((- b) * x) by EUCLID_4:7 ; :: thesis: ( (a - b) * x = (a * x) + (- (b * x)) & (a - b) * x = (a * x) - (b * x) )
hence (a - b) * x = (a * x) + (- (b * x)) by Th3; :: thesis: (a - b) * x = (a * x) - (b * x)
thus (a - b) * x = (a * x) - (b * x) by A1, Th3; :: thesis: verum