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