let r be Real; :: thesis: - (sReal . r) == sReal . (- r)
( (sReal . r) + (sReal . (- r)) == sReal . (r + (- r)) & sReal . (r + (- r)) == uDyadic . 0 ) by Lm13, Th46;
then ( (sReal . r) + (sReal . (- r)) == uDyadic . 0 & uDyadic . 0 = uInt . 0 ) by SURREALO:4, Def5;
then 0_No == (sReal . r) + (sReal . (- r)) by Def1;
then ( - (sReal . r) = (- (sReal . r)) + 0_No & (- (sReal . r)) + 0_No == ((sReal . r) + (sReal . (- r))) + (- (sReal . r)) ) by SURREALR:43;
then A1: - (sReal . r) == (sReal . (- r)) + ((sReal . r) + (- (sReal . r))) by SURREALR:37;
(sReal . r) - (sReal . r) == 0_No by SURREALR:39;
then (sReal . (- r)) + ((sReal . r) + (- (sReal . r))) == (sReal . (- r)) + 0_No by SURREALR:43;
hence - (sReal . r) == sReal . (- r) by A1, SURREALO:4; :: thesis: verum