let x be real number ; :: thesis: for n being Element of NAT
for f being Element of n -tuples_on REAL holds x * (- f) = - (x * f)
let n be Element of NAT ; :: thesis: for f being Element of n -tuples_on REAL holds x * (- f) = - (x * f)
let f be Element of n -tuples_on REAL ; :: thesis: x * (- f) = - (x * f)
thus x * (- f) = x * ((- 1) * f) by RVSUM_1:76
.= ((- 1) * x) * f by RVSUM_1:71
.= - (x * f) by RVSUM_1:71 ; :: thesis: verum