let x be Surreal; :: thesis: for r, r1, r2 being Real holds ((x * (uReal . r)) * (uReal . r1)) * (uReal . r2) == x * (uReal . ((r * r1) * r2))
let r, r1, r2 be Real; :: thesis: ((x * (uReal . r)) * (uReal . r1)) * (uReal . r2) == x * (uReal . ((r * r1) * r2))
( ((x * (uReal . r)) * (uReal . r1)) * (uReal . r2) == (x * (uReal . (r * r1))) * (uReal . r2) & (x * (uReal . (r * r1))) * (uReal . r2) == x * (uReal . ((r * r1) * r2)) ) by Lm1, SURREALR:51;
hence ((x * (uReal . r)) * (uReal . r1)) * (uReal . r2) == x * (uReal . ((r * r1) * r2)) by SURREALO:4; :: thesis: verum