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

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