let n be Nat; :: thesis: for lambda being Real
for x1 being Element of REAL n holds (1 - lambda) * x1 = x1 - (lambda * x1)
let lambda be Real; :: thesis: for x1 being Element of REAL n holds (1 - lambda) * x1 = x1 - (lambda * x1)
let x1 be Element of REAL n; :: thesis: (1 - lambda) * x1 = x1 - (lambda * x1)
(1 - lambda) * x1 = (1 * x1) - (lambda * x1) by EUCLIDLP:11
.= x1 - (lambda * x1) by RVSUM_1:52 ;
hence (1 - lambda) * x1 = x1 - (lambda * x1) ; :: thesis: verum