let x, y, z be Surreal; :: thesis: for r being Real
for s being Surreal st r <> 0 & x is s,y,r _term & x == z holds
z is s,y,r _term
let r be Real; :: thesis: for s being Surreal st r <> 0 & x is s,y,r _term & x == z holds
z is s,y,r _term
let s be Surreal; :: thesis: ( r <> 0 & x is s,y,r _term & x == z implies z is s,y,r _term )
assume A1: ( r <> 0 & x is s,y,r _term & x == z ) ; :: thesis: z is s,y,r _term
then A2: ( not x + (- s) == 0_No & omega-y (x + (- s)) == y & omega-r (x + (- s)) = r ) ;
A3: x + (- s) == z + (- s) by A1, SURREALR:43;
not z + (- s) == 0_No by A2, A3, SURREALO:4;
hence z is s,y,r _term by A1, A3, Th70; :: thesis: verum