let n be Nat; :: thesis: for r, s being Real
for u, v, w being Element of (TOP-REAL n) st (r * u) - (r * v) = (s * w) - (s * u) holds
(r + s) * u = (r * v) + (s * w)
let r, s be Real; :: thesis: for u, v, w being Element of (TOP-REAL n) st (r * u) - (r * v) = (s * w) - (s * u) holds
(r + s) * u = (r * v) + (s * w)
let u, v, w be Element of (TOP-REAL n); :: thesis: ( (r * u) - (r * v) = (s * w) - (s * u) implies (r + s) * u = (r * v) + (s * w) )
assume (r * u) - (r * v) = (s * w) - (s * u) ; :: thesis: (r + s) * u = (r * v) + (s * w)
then ((r * u) - (r * v)) + (s * u) = (s * w) + ((- (s * u)) + (s * u)) by RVSUM_1:15
.= (s * w) + ((((- 1) * s) * u) + (s * u)) by RVSUM_1:49
.= (s * w) + (((- s) + s) * u) by RVSUM_1:50
.= s * w by THJE ;
then (s * w) + (r * v) = (((r * u) + (((- 1) * r) * v)) + (s * u)) + (r * v) by RVSUM_1:49
.= (((r * u) + (s * u)) + (((- 1) * r) * v)) + (r * v) by RVSUM_1:15
.= ((r * u) + (s * u)) + ((((- 1) * r) * v) + (r * v)) by RVSUM_1:15
.= ((r * u) + (s * u)) + (((- r) + r) * v) by RVSUM_1:50
.= (r * u) + (s * u) by THJE ;
hence (r + s) * u = (r * v) + (s * w) by RVSUM_1:50; :: thesis: verum