let s, t, u be Real; :: thesis: for n being Nat
for x being Element of REAL n holds ((s - t) - u) * x = ((s * x) - (t * x)) - (u * x)
let n be Nat; :: thesis: for x being Element of REAL n holds ((s - t) - u) * x = ((s * x) - (t * x)) - (u * x)
let x be Element of REAL n; :: thesis: ((s - t) - u) * x = ((s * x) - (t * x)) - (u * x)
thus ((s - t) - u) * x = ((s - t) * x) - (u * x) by Th11
.= ((s * x) - (t * x)) - (u * x) by Th11 ; :: thesis: verum