let r be Real; :: thesis: - (uReal . r) == uReal . (- r)
A1: ( uReal . r = Unique_No (sReal . r) & uReal . (- r) = Unique_No (sReal . (- r)) ) by Def7;
then A2: ( sReal . r == uReal . r & sReal . (- r) == uReal . (- r) & - (sReal . r) == sReal . (- r) ) by Lm14, SURREALO:def 10;
- (uReal . r) == - (sReal . r) by A1, SURREALR:65, SURREALO:def 10;
then - (uReal . r) == sReal . (- r) by A2, SURREALO:4;
hence - (uReal . r) == uReal . (- r) by A2, SURREALO:4; :: thesis: verum