let x be real number ; :: thesis: for n being Element of NAT
for f, g being Element of n -tuples_on REAL holds x * (f - g) = (x * f) - (x * g)
let n be Element of NAT ; :: thesis: for f, g being Element of n -tuples_on REAL holds x * (f - g) = (x * f) - (x * g)
let f, g be Element of n -tuples_on REAL ; :: thesis: x * (f - g) = (x * f) - (x * g)
thus x * (f - g) = x * (f + (- g)) by RVSUM_1:52
.= (x * f) + (x * (- g)) by RVSUM_1:73
.= (x * f) - (x * g) by Th6 ; :: thesis: verum