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 ( sReal . r1 == uReal . r1 & sReal . r2 == uReal . r2 ) by SURREALO:def 10;
then ( (uReal . r1) + (uReal . r2) == (sReal . r1) + (sReal . r2) & (sReal . r1) + (sReal . r2) == sReal . (r1 + r2) ) by SURREALR:43, Lm13;
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