let y be Surreal; :: thesis: for r being Real
for s being Surreal st r <> 0 holds
s + ((uReal . r) * (No_omega^ y)) is s,y,r _term
let r be Real; :: thesis: for s being Surreal st r <> 0 holds
s + ((uReal . r) * (No_omega^ y)) is s,y,r _term
let s be Surreal; :: thesis: ( r <> 0 implies s + ((uReal . r) * (No_omega^ y)) is s,y,r _term )
assume A1: r <> 0 ; :: thesis: s + ((uReal . r) * (No_omega^ y)) is s,y,r _term
set R = uReal . r;
set N = No_omega^ y;
set sRNs = (s + ((uReal . r) * (No_omega^ y))) + (- s);
s - s == 0_No by SURREALR:39;
then A2: ( (s + ((uReal . r) * (No_omega^ y))) + (- s) = ((uReal . r) * (No_omega^ y)) + (s + (- s)) & ((uReal . r) * (No_omega^ y)) + (s + (- s)) == ((uReal . r) * (No_omega^ y)) + 0_No & ((uReal . r) * (No_omega^ y)) + 0_No = (uReal . r) * (No_omega^ y) ) by SURREALR:43, SURREALR:37;
A3: not (uReal . r) * (No_omega^ y) == 0_No by A1, Th67;
then A4: not (s + ((uReal . r) * (No_omega^ y))) + (- s) == 0_No by A2, SURREALO:4;
A5: omega-y ((uReal . r) * (No_omega^ y)) = Unique_No y by A1, Th68;
|.((uReal . r) * (No_omega^ y)).| is positive by A1, Th67, Th36;
then |.((s + ((uReal . r) * (No_omega^ y))) + (- s)).|,|.((uReal . r) * (No_omega^ y)).| are_commensurate by A2, Th48, Th8;
then A6: ( omega-y ((s + ((uReal . r) * (No_omega^ y))) + (- s)) = Unique_No y & Unique_No y == y ) by SURREALO:def 10, A4, A5, Th61, A3;
then No_omega^ (omega-y ((s + ((uReal . r) * (No_omega^ y))) + (- s))) == No_omega^ y by Lm5;
then (No_omega^ (omega-y ((s + ((uReal . r) * (No_omega^ y))) + (- s)))) * (uReal . r) == (No_omega^ y) * (uReal . r) by SURREALR:51;
then - ((No_omega^ (omega-y ((s + ((uReal . r) * (No_omega^ y))) + (- s)))) * (uReal . r)) == - ((No_omega^ y) * (uReal . r)) by SURREALR:10;
then ( ((s + ((uReal . r) * (No_omega^ y))) + (- s)) - ((No_omega^ (omega-y ((s + ((uReal . r) * (No_omega^ y))) + (- s)))) * (uReal . r)) == ((No_omega^ y) * (uReal . r)) - ((No_omega^ y) * (uReal . r)) & ((No_omega^ y) * (uReal . r)) - ((No_omega^ y) * (uReal . r)) == 0_No ) by A2, SURREALR:43, SURREALR:39;
then ((s + ((uReal . r) * (No_omega^ y))) + (- s)) + (- ((No_omega^ (omega-y ((s + ((uReal . r) * (No_omega^ y))) + (- s)))) * (uReal . r))) == 0_No by SURREALO:4;
then |.(((s + ((uReal . r) * (No_omega^ y))) + (- s)) + (- ((No_omega^ (omega-y ((s + ((uReal . r) * (No_omega^ y))) + (- s)))) * (uReal . r)))).| == 0_No by Def6;
then |.(((s + ((uReal . r) * (No_omega^ y))) + (- s)) - ((No_omega^ (omega-y ((s + ((uReal . r) * (No_omega^ y))) + (- s)))) * (uReal . r))).| infinitely< |.((s + ((uReal . r) * (No_omega^ y))) + (- s)).| by A4, Th64;
hence s + ((uReal . r) * (No_omega^ y)) is s,y,r _term by A1, A4, Def8, A6; :: thesis: verum