let r1, r2 be Real; :: thesis: (uReal . r1) * (uReal . r2) == uReal . (r1 * r2)
( uReal . r1 = Unique_No (sReal . r1) & uReal . r2 = Unique_No (sReal . r2) ) by Def7;
then ( (uReal . r1) * (uReal . r2) == (uReal . r1) * (sReal . r2) & (uReal . r1) * (sReal . r2) == (sReal . r1) * (sReal . r2) ) by SURREALO:def 10, SURREALR:51;
then ( (uReal . r1) * (uReal . r2) == (sReal . r1) * (sReal . r2) & (sReal . r1) * (sReal . r2) == sReal . (r1 * r2) ) by Lm19, SURREALO:4;
then A1: (uReal . r1) * (uReal . r2) == sReal . (r1 * r2) by SURREALO:4;
uReal . (r1 * r2) = Unique_No (sReal . (r1 * r2)) by Def7;
then sReal . (r1 * r2) == uReal . (r1 * r2) by SURREALO:def 10;
hence (uReal . r1) * (uReal . r2) == uReal . (r1 * r2) by A1, SURREALO:4; :: thesis: verum