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