let s, t, u be Real; :: thesis: for n being Nat
for x being Element of REAL n holds
( (s / t) * (u * x) = ((s * u) / t) * x & (1 / t) * (u * x) = (u / t) * x )
let n be Nat; :: thesis: for x being Element of REAL n holds
( (s / t) * (u * x) = ((s * u) / t) * x & (1 / t) * (u * x) = (u / t) * x )
let x be Element of REAL n; :: thesis: ( (s / t) * (u * x) = ((s * u) / t) * x & (1 / t) * (u * x) = (u / t) * x )
thus (s / t) * (u * x) = ((s / t) * u) * x by EUCLID_4:4
.= ((s * u) / t) * x by XCMPLX_1:74 ; :: thesis: (1 / t) * (u * x) = (u / t) * x
thus (1 / t) * (u * x) = ((1 / t) * u) * x by EUCLID_4:4
.= (u / t) * x by XCMPLX_1:99 ; :: thesis: verum