let s, t, u be Real; :: thesis: for n being Element of NAT
for x, y being Element of REAL n holds x - (((s + t) + u) * y) = ((x + ((- s) * y)) + ((- t) * y)) + ((- u) * y)
let n be Element of NAT ; :: thesis: for x, y being Element of REAL n holds x - (((s + t) + u) * y) = ((x + ((- s) * y)) + ((- t) * y)) + ((- u) * y)
let x, y be Element of REAL n; :: thesis: x - (((s + t) + u) * y) = ((x + ((- s) * y)) + ((- t) * y)) + ((- u) * y)
thus x - (((s + t) + u) * y) = x - (((s + t) * y) + (u * y)) by EUCLID_4:7
.= x - (((s * y) + (t * y)) + (u * y)) by EUCLID_4:7
.= x + ((((- s) * y) + ((- t) * y)) + ((- u) * y)) by Th19
.= (x + (((- s) * y) + ((- t) * y))) + ((- u) * y) by RVSUM_1:15
.= ((x + ((- s) * y)) + ((- t) * y)) + ((- u) * y) by RVSUM_1:15 ; :: thesis: verum