let s, z be Surreal; :: thesis: for r, e being Real holds
( s + ((uReal . (r + e)) * z) == (s + ((uReal . r) * z)) + ((uReal . e) * z) & s + ((uReal . (r - e)) * z) == (s + ((uReal . r) * z)) - ((uReal . e) * z) )
let r, e be Real; :: thesis: ( s + ((uReal . (r + e)) * z) == (s + ((uReal . r) * z)) + ((uReal . e) * z) & s + ((uReal . (r - e)) * z) == (s + ((uReal . r) * z)) - ((uReal . e) * z) )
thus s + ((uReal . (r + e)) * z) == (s + ((uReal . r) * z)) + ((uReal . e) * z) by Lm1; :: thesis: s + ((uReal . (r - e)) * z) == (s + ((uReal . r) * z)) - ((uReal . e) * z)
A1: s + ((uReal . (r + (- e))) * z) == (s + ((uReal . r) * z)) + ((uReal . (- e)) * z) by Lm1;
( z * (uReal . (- e)) == z * (- (uReal . e)) & z * (- (uReal . e)) = - (z * (uReal . e)) ) by SURREALR:54, SURREALR:58, SURREALN:56;
then (s + ((uReal . r) * z)) + ((uReal . (- e)) * z) == (s + ((uReal . r) * z)) + (- ((uReal . e) * z)) by SURREALR:43;
hence s + ((uReal . (r - e)) * z) == (s + ((uReal . r) * z)) - ((uReal . e) * z) by A1, SURREALO:10; :: thesis: verum