let x, y be Surreal; :: thesis: (No_omega^ x) * (No_omega^ y) == No_omega^ (x + y)
defpred S₁[ Ordinal] means for x, y being Surreal st (born x) (+) (born y) = $1 holds
(No_omega^ x) * (No_omega^ y) == No_omega^ (x + y);
A1: for D being Ordinal st ( for C being Ordinal st C in D holds
S₁[C] ) holds
S₁[D]

proof

let D be Ordinal; :: thesis: ( ( for C being Ordinal st C in D holds
S₁[C] ) implies S₁[D] )
assume A2: for C being Ordinal st C in D holds
S₁[C] ; :: thesis: S₁[D]
let x, y be Surreal; :: thesis: ( (born x) (+) (born y) = D implies (No_omega^ x) * (No_omega^ y) == No_omega^ (x + y) )
assume A3: (born x) (+) (born y) = D ; :: thesis: (No_omega^ x) * (No_omega^ y) == No_omega^ (x + y)
set Nx = No_omega^ x;
set Ny = No_omega^ y;
set xy = x + y;
set Nxy = No_omega^ (x + y);
A4: (No_omega^ x) * (No_omega^ y) = [((comp ((L_ (No_omega^ x)),(No_omega^ x),(No_omega^ y),(L_ (No_omega^ y)))) \/ (comp ((R_ (No_omega^ x)),(No_omega^ x),(No_omega^ y),(R_ (No_omega^ y))))),((comp ((L_ (No_omega^ x)),(No_omega^ x),(No_omega^ y),(R_ (No_omega^ y)))) \/ (comp ((R_ (No_omega^ x)),(No_omega^ x),(No_omega^ y),(L_ (No_omega^ y)))))] by SURREALR:50;
A5: x + y = [(((L_ x) ++ {y}) \/ ({x} ++ (L_ y))),(((R_ x) ++ {y}) \/ ({x} ++ (R_ y)))] by SURREALR:28;
A6: for a being Surreal st a in L_ ((No_omega^ x) * (No_omega^ y)) holds
ex b being Surreal st
( b in L_ (No_omega^ (x + y)) & a <= b )

proof

let a be Surreal; :: thesis: ( a in L_ ((No_omega^ x) * (No_omega^ y)) implies ex b being Surreal st
( b in L_ (No_omega^ (x + y)) & a <= b ) )
assume A7: a in L_ ((No_omega^ x) * (No_omega^ y)) ; :: thesis: ex b being Surreal st
( b in L_ (No_omega^ (x + y)) & a <= b )

per cases ( a in comp ((R_ (No_omega^ x)),(No_omega^ x),(No_omega^ y),(R_ (No_omega^ y))) or a in comp ((L_ (No_omega^ x)),(No_omega^ x),(No_omega^ y),(L_ (No_omega^ y))) ) by A7, A4, XBOOLE_0:def 3;

suppose a in comp ((R_ (No_omega^ x)),(No_omega^ x),(No_omega^ y),(R_ (No_omega^ y))) ; :: thesis: ex b being Surreal st
( b in L_ (No_omega^ (x + y)) & a <= b )

then consider x1, y1 being Surreal such that
A8: ( a = ((x1 * (No_omega^ y)) + ((No_omega^ x) * y1)) - (x1 * y1) & x1 in R_ (No_omega^ x) & y1 in R_ (No_omega^ y) ) by SURREALR:def 15;
consider xL being Surreal, r being positive Real such that
A9: ( xL in R_ x & x1 = (No_omega^ xL) * (uReal . r) ) by A8, Th23;
consider yL being Surreal, s being positive Real such that
A10: ( yL in R_ y & y1 = (No_omega^ yL) * (uReal . s) ) by A8, Th23;
A11: 0_No < y1 by A10, SURREALI:def 8;
A12: 0_No < x1 by A9, SURREALI:def 8;
set H = uReal . (1 / 2);
(1 / 2) + (1 / 2) = 1 ;
then ( ((x1 * y1) * (uReal . (1 / 2))) + ((x1 * y1) * (uReal . (1 / 2))) == (x1 * y1) * ((uReal . (1 / 2)) + (uReal . (1 / 2))) & (x1 * y1) * ((uReal . (1 / 2)) + (uReal . (1 / 2))) == (x1 * y1) * 1_No & (x1 * y1) * 1_No = x1 * y1 ) by SURREALN:55, SURREALN:48, SURREALR:51, SURREALR:67;
then A13: ((x1 * y1) * (uReal . (1 / 2))) + ((x1 * y1) * (uReal . (1 / 2))) == x1 * y1 by SURREALO:4;
( x in {x} & {x} << R_ x ) by TARSKI:def 1, SURREALO:11;
then No_omega^ x infinitely< No_omega^ xL by A9, Th25;
then No_omega^ x infinitely< x1 by A9, Th13;
then No_omega^ x infinitely< (uReal . (1 / 2)) * x1 by Th13;
then No_omega^ x < (uReal . (1 / 2)) * x1 by Th9;
then ( (No_omega^ x) * y1 <= ((uReal . (1 / 2)) * x1) * y1 & ((uReal . (1 / 2)) * x1) * y1 == (uReal . (1 / 2)) * (x1 * y1) ) by SURREALR:70, A11, SURREALR:69;
then A14: (No_omega^ x) * y1 <= (uReal . (1 / 2)) * (x1 * y1) by SURREALO:4;
( y in {y} & {y} << R_ y ) by TARSKI:def 1, SURREALO:11;
then No_omega^ y infinitely< No_omega^ yL by A10, Th25;
then No_omega^ y infinitely< y1 by Th13, A10;
then No_omega^ y infinitely< (uReal . (1 / 2)) * y1 by Th13;
then No_omega^ y < (uReal . (1 / 2)) * y1 by Th9;
then ( (No_omega^ y) * x1 <= ((uReal . (1 / 2)) * y1) * x1 & ((uReal . (1 / 2)) * y1) * x1 == (uReal . (1 / 2)) * (x1 * y1) ) by SURREALR:70, A12, SURREALR:69;
then (No_omega^ y) * x1 <= (uReal . (1 / 2)) * (x1 * y1) by SURREALO:4;
then ((No_omega^ x) * y1) + ((No_omega^ y) * x1) <= ((uReal . (1 / 2)) * (x1 * y1)) + ((uReal . (1 / 2)) * (x1 * y1)) by SURREALR:43, A14;
then ((No_omega^ x) * y1) + ((No_omega^ y) * x1) <= x1 * y1 by A13, SURREALO:4;
then ( a <= 0_No & 0_No in L_ (No_omega^ (x + y)) ) by A8, Th22, SURREALR:45;
hence ex b being Surreal st
( b in L_ (No_omega^ (x + y)) & a <= b ) ; :: thesis: verum

end;

suppose a in comp ((L_ (No_omega^ x)),(No_omega^ x),(No_omega^ y),(L_ (No_omega^ y))) ; :: thesis: ex b being Surreal st
( b in L_ (No_omega^ (x + y)) & a <= b )

then consider x1, y1 being Surreal such that
A15: ( a = ((x1 * (No_omega^ y)) + ((No_omega^ x) * y1)) - (x1 * y1) & x1 in L_ (No_omega^ x) & y1 in L_ (No_omega^ y) ) by SURREALR:def 15;

per cases ( x1 = 0_No or ex xL being Surreal ex r being positive Real st
( xL in L_ x & x1 = (No_omega^ xL) * (uReal . r) ) ) by A15, Th22;

suppose A16: x1 = 0_No ; :: thesis: ex b being Surreal st
( b in L_ (No_omega^ (x + y)) & a <= b )

per cases ( y1 = 0_No or ex yL being Surreal ex s being positive Real st
( yL in L_ y & y1 = (No_omega^ yL) * (uReal . s) ) ) by A15, Th22;

suppose y1 = 0_No ; :: thesis: ex b being Surreal st
( b in L_ (No_omega^ (x + y)) & a <= b )

then a in L_ (No_omega^ (x + y)) by Th22, A16, A15;
hence ex b being Surreal st
( b in L_ (No_omega^ (x + y)) & a <= b ) ; :: thesis: verum

end;

suppose ex yL being Surreal ex s being positive Real st
( yL in L_ y & y1 = (No_omega^ yL) * (uReal . s) ) ; :: thesis: ex b being Surreal st
( b in L_ (No_omega^ (x + y)) & a <= b )

then consider yL being Surreal, s being positive Real such that
A17: ( yL in L_ y & y1 = (No_omega^ yL) * (uReal . s) ) ;
yL in (L_ y) \/ (R_ y) by A17, XBOOLE_0:def 3;
then A18: (born x) (+) (born yL) in (born x) (+) (born y) by ORDINAL7:94, SURREALO:1;
A19: ( a == ((No_omega^ x) * (No_omega^ yL)) * (uReal . s) & ((No_omega^ x) * (No_omega^ yL)) * (uReal . s) == (No_omega^ (x + yL)) * (uReal . s) ) by A17, A18, A3, A2, SURREALR:69, SURREALR:54, A15, A16;
x in {x} by TARSKI:def 1;
then x + yL in {x} ++ (L_ y) by A17, SURREALR:def 8;
then x + yL in L_ (x + y) by A5, XBOOLE_0:def 3;
then (No_omega^ (x + yL)) * (uReal . s) in L_ (No_omega^ (x + y)) by Th22;
hence ex b being Surreal st
( b in L_ (No_omega^ (x + y)) & a <= b ) by A19, SURREALO:9; :: thesis: verum

end;

end;

end;

suppose ex xL being Surreal ex r being positive Real st
( xL in L_ x & x1 = (No_omega^ xL) * (uReal . r) ) ; :: thesis: ex b being Surreal st
( b in L_ (No_omega^ (x + y)) & a <= b )

then consider xL being Surreal, r being positive Real such that
A20: ( xL in L_ x & x1 = (No_omega^ xL) * (uReal . r) ) ;
A21: xL in (L_ x) \/ (R_ x) by A20, XBOOLE_0:def 3;
then born xL in born x by SURREALO:1;
then A22: (No_omega^ xL) * (No_omega^ y) == No_omega^ (xL + y) by A3, A2, ORDINAL7:94;
A23: ( ((uReal . r) * (No_omega^ xL)) * (No_omega^ y) == (uReal . r) * ((No_omega^ xL) * (No_omega^ y)) & (uReal . r) * ((No_omega^ xL) * (No_omega^ y)) == (uReal . r) * (No_omega^ (xL + y)) ) by A22, SURREALR:69, SURREALR:54;
then A24: ((uReal . r) * (No_omega^ xL)) * (No_omega^ y) == (uReal . r) * (No_omega^ (xL + y)) by SURREALO:9;

per cases ( y1 = 0_No or ex yL being Surreal ex s being positive Real st
( yL in L_ y & y1 = (No_omega^ yL) * (uReal . s) ) ) by A15, Th22;

suppose A25: y1 = 0_No ; :: thesis: ex b being Surreal st
( b in L_ (No_omega^ (x + y)) & a <= b )

y in {y} by TARSKI:def 1;
then xL + y in (L_ x) ++ {y} by A20, SURREALR:def 8;
then xL + y in L_ (x + y) by A5, XBOOLE_0:def 3;
then (No_omega^ (xL + y)) * (uReal . r) in L_ (No_omega^ (x + y)) by Th22;
hence ex b being Surreal st
( b in L_ (No_omega^ (x + y)) & a <= b ) by A20, A23, SURREALO:9, A15, A25; :: thesis: verum

end;

suppose ex yL being Surreal ex s being positive Real st
( yL in L_ y & y1 = (No_omega^ yL) * (uReal . s) ) ; :: thesis: ex b being Surreal st
( b in L_ (No_omega^ (x + y)) & a <= b )

then consider yL being Surreal, s being positive Real such that
A26: ( yL in L_ y & y1 = (No_omega^ yL) * (uReal . s) ) ;
yL in (L_ y) \/ (R_ y) by A26, XBOOLE_0:def 3;
then ( (born xL) (+) (born yL) in (born x) (+) (born yL) & (born x) (+) (born yL) in (born x) (+) (born y) ) by A21, SURREALO:1, ORDINAL7:94;
then ( (No_omega^ x) * y1 == ((No_omega^ x) * (No_omega^ yL)) * (uReal . s) & ((No_omega^ x) * (No_omega^ yL)) * (uReal . s) == (No_omega^ (x + yL)) * (uReal . s) ) by A3, A2, A26, SURREALR:69, SURREALR:54;
then A27: (No_omega^ x) * y1 == (No_omega^ (x + yL)) * (uReal . s) by SURREALO:9;
A28: ( - (x1 * y1) <= - 0_No & - 0_No = 0_No ) by A20, A26, SURREALI:def 8, SURREALR:10;
x in {x} by TARSKI:def 1;
then x + yL in {x} ++ (L_ y) by A26, SURREALR:def 8;
then A29: x + yL in L_ (x + y) by A5, XBOOLE_0:def 3;
y in {y} by TARSKI:def 1;
then xL + y in (L_ x) ++ {y} by A20, SURREALR:def 8;
then A30: xL + y in L_ (x + y) by A5, XBOOLE_0:def 3;

per cases ( xL + y <= x + yL or x + yL <= xL + y ) ;

suppose xL + y <= x + yL ; :: thesis: ex b being Surreal st
( b in L_ (No_omega^ (x + y)) & a <= b )

then A31: No_omega^ (xL + y) <= No_omega^ (x + yL) by Lm5;
0_No <= uReal . r by SURREALI:def 8;
then (No_omega^ (xL + y)) * (uReal . r) <= (No_omega^ (x + yL)) * (uReal . r) by A31, SURREALR:75;
then x1 * (No_omega^ y) <= (No_omega^ (x + yL)) * (uReal . r) by A20, A24, SURREALO:4;
then ( (x1 * (No_omega^ y)) + ((No_omega^ x) * y1) <= ((No_omega^ (x + yL)) * (uReal . r)) + ((No_omega^ (x + yL)) * (uReal . s)) & ((No_omega^ (x + yL)) * (uReal . r)) + ((No_omega^ (x + yL)) * (uReal . s)) == (No_omega^ (x + yL)) * ((uReal . r) + (uReal . s)) ) by A27, SURREALR:43, SURREALR:67;
then (x1 * (No_omega^ y)) + ((No_omega^ x) * y1) <= (No_omega^ (x + yL)) * ((uReal . r) + (uReal . s)) by SURREALO:4;
then A32: ( ((x1 * (No_omega^ y)) + ((No_omega^ x) * y1)) + (- (x1 * y1)) <= ((No_omega^ (x + yL)) * ((uReal . r) + (uReal . s))) + 0_No & ((No_omega^ (x + yL)) * ((uReal . r) + (uReal . s))) + 0_No = (No_omega^ (x + yL)) * ((uReal . r) + (uReal . s)) ) by A28, SURREALR:43;
A33: (No_omega^ (x + yL)) * ((uReal . r) + (uReal . s)) == (No_omega^ (x + yL)) * (uReal . (r + s)) by SURREALR:54, SURREALN:55;
(No_omega^ (x + yL)) * (uReal . (r + s)) in L_ (No_omega^ (x + y)) by A29, Th22;
hence ex b being Surreal st
( b in L_ (No_omega^ (x + y)) & a <= b ) by A33, A32, A15, SURREALO:4; :: thesis: verum

end;

suppose x + yL <= xL + y ; :: thesis: ex b being Surreal st
( b in L_ (No_omega^ (x + y)) & a <= b )

then A34: No_omega^ (x + yL) <= No_omega^ (xL + y) by Lm5;
0_No <= uReal . s by SURREALI:def 8;
then (No_omega^ (x + yL)) * (uReal . s) <= (No_omega^ (xL + y)) * (uReal . s) by A34, SURREALR:75;
then (No_omega^ x) * y1 <= (No_omega^ (xL + y)) * (uReal . s) by A27, SURREALO:4;
then ( (x1 * (No_omega^ y)) + ((No_omega^ x) * y1) <= ((No_omega^ (xL + y)) * (uReal . r)) + ((No_omega^ (xL + y)) * (uReal . s)) & ((No_omega^ (xL + y)) * (uReal . r)) + ((No_omega^ (xL + y)) * (uReal . s)) == (No_omega^ (xL + y)) * ((uReal . r) + (uReal . s)) ) by A20, A24, SURREALR:43, SURREALR:67;
then (x1 * (No_omega^ y)) + ((No_omega^ x) * y1) <= (No_omega^ (xL + y)) * ((uReal . r) + (uReal . s)) by SURREALO:4;
then A35: ( ((x1 * (No_omega^ y)) + ((No_omega^ x) * y1)) + (- (x1 * y1)) <= ((No_omega^ (xL + y)) * ((uReal . r) + (uReal . s))) + 0_No & ((No_omega^ (xL + y)) * ((uReal . r) + (uReal . s))) + 0_No = (No_omega^ (xL + y)) * ((uReal . r) + (uReal . s)) ) by A28, SURREALR:43;
A36: (No_omega^ (xL + y)) * ((uReal . r) + (uReal . s)) == (No_omega^ (xL + y)) * (uReal . (r + s)) by SURREALR:54, SURREALN:55;
take Y2 = (No_omega^ (xL + y)) * (uReal . (r + s)); :: thesis: ( Y2 in L_ (No_omega^ (x + y)) & a <= Y2 )
thus ( Y2 in L_ (No_omega^ (x + y)) & a <= Y2 ) by A36, A30, Th22, A35, A15, SURREALO:4; :: thesis: verum

end;

end;

end;

end;

end;

end;

end;

end;

end;

A37: for a being Surreal st a in R_ (No_omega^ (x + y)) holds
ex b being Surreal st
( b in R_ ((No_omega^ x) * (No_omega^ y)) & b <= a )

proof

let a be Surreal; :: thesis: ( a in R_ (No_omega^ (x + y)) implies ex b being Surreal st
( b in R_ ((No_omega^ x) * (No_omega^ y)) & b <= a ) )
assume A38: a in R_ (No_omega^ (x + y)) ; :: thesis: ex b being Surreal st
( b in R_ ((No_omega^ x) * (No_omega^ y)) & b <= a )
consider xR being Surreal, r being positive Real such that
A39: ( xR in R_ (x + y) & a = (No_omega^ xR) * (uReal . r) ) by A38, Th23;

per cases ( xR in (R_ x) ++ {y} or xR in {x} ++ (R_ y) ) by A39, A5, XBOOLE_0:def 3;

suppose xR in (R_ x) ++ {y} ; :: thesis: ex b being Surreal st
( b in R_ ((No_omega^ x) * (No_omega^ y)) & b <= a )

then consider x1, y1 being Surreal such that
A40: ( x1 in R_ x & y1 in {y} & xR = x1 + y1 ) by SURREALR:def 8;
set R = (No_omega^ x1) * (uReal . r);
set A = ((((No_omega^ x1) * (uReal . r)) * (No_omega^ y)) + ((No_omega^ x) * 0_No)) - (((No_omega^ x1) * (uReal . r)) * 0_No);
A41: (No_omega^ x1) * (uReal . r) in R_ (No_omega^ x) by A40, Th23;
0_No in L_ (No_omega^ y) by Th22;
then ((((No_omega^ x1) * (uReal . r)) * (No_omega^ y)) + ((No_omega^ x) * 0_No)) - (((No_omega^ x1) * (uReal . r)) * 0_No) in comp ((R_ (No_omega^ x)),(No_omega^ x),(No_omega^ y),(L_ (No_omega^ y))) by A41, SURREALR:def 15;
then A42: ((((No_omega^ x1) * (uReal . r)) * (No_omega^ y)) + ((No_omega^ x) * 0_No)) - (((No_omega^ x1) * (uReal . r)) * 0_No) in R_ ((No_omega^ x) * (No_omega^ y)) by XBOOLE_0:def 3, A4;
A43: a = (No_omega^ (x1 + y)) * (uReal . r) by A39, A40, TARSKI:def 1;
x1 in (L_ x) \/ (R_ x) by A40, XBOOLE_0:def 3;
then (born x1) (+) (born y) in (born x) (+) (born y) by ORDINAL7:94, SURREALO:1;
then ( a == ((No_omega^ y) * (No_omega^ x1)) * (uReal . r) & ((No_omega^ y) * (No_omega^ x1)) * (uReal . r) == (No_omega^ y) * ((No_omega^ x1) * (uReal . r)) ) by A3, A2, SURREALR:54, A43, SURREALR:69;
hence ex b being Surreal st
( b in R_ ((No_omega^ x) * (No_omega^ y)) & b <= a ) by A42, SURREALO:4; :: thesis: verum

end;

suppose xR in {x} ++ (R_ y) ; :: thesis: ex b being Surreal st
( b in R_ ((No_omega^ x) * (No_omega^ y)) & b <= a )

then consider x1, y1 being Surreal such that
A44: ( x1 in {x} & y1 in R_ y & xR = x1 + y1 ) by SURREALR:def 8;
set R = (No_omega^ y1) * (uReal . r);
set A = ((0_No * (No_omega^ y)) + ((No_omega^ x) * ((No_omega^ y1) * (uReal . r)))) - (0_No * ((No_omega^ y1) * (uReal . r)));
A45: (No_omega^ y1) * (uReal . r) in R_ (No_omega^ y) by A44, Th23;
0_No in L_ (No_omega^ x) by Th22;
then ((0_No * (No_omega^ y)) + ((No_omega^ x) * ((No_omega^ y1) * (uReal . r)))) - (0_No * ((No_omega^ y1) * (uReal . r))) in comp ((L_ (No_omega^ x)),(No_omega^ x),(No_omega^ y),(R_ (No_omega^ y))) by A45, SURREALR:def 15;
then A46: ((0_No * (No_omega^ y)) + ((No_omega^ x) * ((No_omega^ y1) * (uReal . r)))) - (0_No * ((No_omega^ y1) * (uReal . r))) in R_ ((No_omega^ x) * (No_omega^ y)) by XBOOLE_0:def 3, A4;
A47: a = (No_omega^ (x + y1)) * (uReal . r) by A39, A44, TARSKI:def 1;
y1 in (L_ y) \/ (R_ y) by A44, XBOOLE_0:def 3;
then (born x) (+) (born y1) in (born x) (+) (born y) by ORDINAL7:94, SURREALO:1;
then ( a == ((No_omega^ x) * (No_omega^ y1)) * (uReal . r) & ((No_omega^ x) * (No_omega^ y1)) * (uReal . r) == (No_omega^ x) * ((No_omega^ y1) * (uReal . r)) ) by A3, A2, SURREALR:54, A47, SURREALR:69;
hence ex b being Surreal st
( b in R_ ((No_omega^ x) * (No_omega^ y)) & b <= a ) by A46, SURREALO:4; :: thesis: verum

end;

end;

end;

A48: ( (No_omega^ x) * (No_omega^ y) = [(L_ ((No_omega^ x) * (No_omega^ y))),(R_ ((No_omega^ x) * (No_omega^ y)))] & No_omega^ (x + y) = [(L_ (No_omega^ (x + y))),(R_ (No_omega^ (x + y)))] ) ;
A49: for a being Surreal st a in L_ (No_omega^ (x + y)) holds
ex b being Surreal st
( b in L_ ((No_omega^ x) * (No_omega^ y)) & a <= b )

proof

let a be Surreal; :: thesis: ( a in L_ (No_omega^ (x + y)) implies ex b being Surreal st
( b in L_ ((No_omega^ x) * (No_omega^ y)) & a <= b ) )
assume A50: a in L_ (No_omega^ (x + y)) ; :: thesis: ex b being Surreal st
( b in L_ ((No_omega^ x) * (No_omega^ y)) & a <= b )

per cases ( a = 0_No or not a = 0_No ) ;

suppose A51: a = 0_No ; :: thesis: ex b being Surreal st
( b in L_ ((No_omega^ x) * (No_omega^ y)) & a <= b )

set A = ((0_No * (No_omega^ y)) + ((No_omega^ x) * 0_No)) - (0_No * 0_No);
( 0_No in L_ (No_omega^ x) & 0_No in L_ (No_omega^ y) ) by Th22;
then ((0_No * (No_omega^ y)) + ((No_omega^ x) * 0_No)) - (0_No * 0_No) in comp ((L_ (No_omega^ x)),(No_omega^ x),(No_omega^ y),(L_ (No_omega^ y))) by SURREALR:def 15;
then ((0_No * (No_omega^ y)) + ((No_omega^ x) * 0_No)) - (0_No * 0_No) in L_ ((No_omega^ x) * (No_omega^ y)) by XBOOLE_0:def 3, A4;
hence ex b being Surreal st
( b in L_ ((No_omega^ x) * (No_omega^ y)) & a <= b ) by A51; :: thesis: verum

end;

suppose not a = 0_No ; :: thesis: ex b being Surreal st
( b in L_ ((No_omega^ x) * (No_omega^ y)) & a <= b )

then consider xR being Surreal, r being positive Real such that
A52: ( xR in L_ (x + y) & a = (No_omega^ xR) * (uReal . r) ) by A50, Th22;

per cases ( xR in (L_ x) ++ {y} or xR in {x} ++ (L_ y) ) by A52, A5, XBOOLE_0:def 3;

suppose xR in (L_ x) ++ {y} ; :: thesis: ex b being Surreal st
( b in L_ ((No_omega^ x) * (No_omega^ y)) & a <= b )

then consider x1, y1 being Surreal such that
A53: ( x1 in L_ x & y1 in {y} & xR = x1 + y1 ) by SURREALR:def 8;
set R = (No_omega^ x1) * (uReal . r);
set A = ((((No_omega^ x1) * (uReal . r)) * (No_omega^ y)) + ((No_omega^ x) * 0_No)) - (((No_omega^ x1) * (uReal . r)) * 0_No);
A54: (No_omega^ x1) * (uReal . r) in L_ (No_omega^ x) by A53, Th22;
0_No in L_ (No_omega^ y) by Th22;
then ((((No_omega^ x1) * (uReal . r)) * (No_omega^ y)) + ((No_omega^ x) * 0_No)) - (((No_omega^ x1) * (uReal . r)) * 0_No) in comp ((L_ (No_omega^ x)),(No_omega^ x),(No_omega^ y),(L_ (No_omega^ y))) by A54, SURREALR:def 15;
then A55: ((((No_omega^ x1) * (uReal . r)) * (No_omega^ y)) + ((No_omega^ x) * 0_No)) - (((No_omega^ x1) * (uReal . r)) * 0_No) in L_ ((No_omega^ x) * (No_omega^ y)) by XBOOLE_0:def 3, A4;
A56: a = (No_omega^ (x1 + y)) * (uReal . r) by A53, TARSKI:def 1, A52;
x1 in (L_ x) \/ (R_ x) by A53, XBOOLE_0:def 3;
then (born x1) (+) (born y) in (born x) (+) (born y) by ORDINAL7:94, SURREALO:1;
then ( a == ((No_omega^ y) * (No_omega^ x1)) * (uReal . r) & ((No_omega^ y) * (No_omega^ x1)) * (uReal . r) == (No_omega^ y) * ((No_omega^ x1) * (uReal . r)) ) by A3, A2, SURREALR:54, A56, SURREALR:69;
hence ex b being Surreal st
( b in L_ ((No_omega^ x) * (No_omega^ y)) & a <= b ) by A55, SURREALO:4; :: thesis: verum

end;

suppose xR in {x} ++ (L_ y) ; :: thesis: ex b being Surreal st
( b in L_ ((No_omega^ x) * (No_omega^ y)) & a <= b )

then consider x1, y1 being Surreal such that
A57: ( x1 in {x} & y1 in L_ y & xR = x1 + y1 ) by SURREALR:def 8;
A58: x1 = x by A57, TARSKI:def 1;
set R = (No_omega^ y1) * (uReal . r);
set A = ((0_No * (No_omega^ y)) + ((No_omega^ x) * ((No_omega^ y1) * (uReal . r)))) - (0_No * ((No_omega^ y1) * (uReal . r)));
A59: (No_omega^ y1) * (uReal . r) in L_ (No_omega^ y) by A57, Th22;
0_No in L_ (No_omega^ x) by Th22;
then ((0_No * (No_omega^ y)) + ((No_omega^ x) * ((No_omega^ y1) * (uReal . r)))) - (0_No * ((No_omega^ y1) * (uReal . r))) in comp ((L_ (No_omega^ x)),(No_omega^ x),(No_omega^ y),(L_ (No_omega^ y))) by A59, SURREALR:def 15;
then A60: ((0_No * (No_omega^ y)) + ((No_omega^ x) * ((No_omega^ y1) * (uReal . r)))) - (0_No * ((No_omega^ y1) * (uReal . r))) in L_ ((No_omega^ x) * (No_omega^ y)) by XBOOLE_0:def 3, A4;
y1 in (L_ y) \/ (R_ y) by A57, XBOOLE_0:def 3;
then (born x) (+) (born y1) in (born x) (+) (born y) by ORDINAL7:94, SURREALO:1;
then ( a == ((No_omega^ x) * (No_omega^ y1)) * (uReal . r) & ((No_omega^ x) * (No_omega^ y1)) * (uReal . r) == (No_omega^ x) * ((No_omega^ y1) * (uReal . r)) ) by A3, A2, SURREALR:54, A52, A57, A58, SURREALR:69;
hence ex b being Surreal st
( b in L_ ((No_omega^ x) * (No_omega^ y)) & a <= b ) by A60, SURREALO:4; :: thesis: verum

end;

end;

end;

end;

end;

A61: for x, y, a being Surreal st (born x) (+) (born y) = D & a in comp ((L_ (No_omega^ x)),(No_omega^ x),(No_omega^ y),(R_ (No_omega^ y))) holds
ex b being Surreal st
( b in R_ (No_omega^ (x + y)) & b <= a )

proof

let x, y, a be Surreal; :: thesis: ( (born x) (+) (born y) = D & a in comp ((L_ (No_omega^ x)),(No_omega^ x),(No_omega^ y),(R_ (No_omega^ y))) implies ex b being Surreal st
( b in R_ (No_omega^ (x + y)) & b <= a ) )
assume A62: (born x) (+) (born y) = D ; :: thesis: ( not a in comp ((L_ (No_omega^ x)),(No_omega^ x),(No_omega^ y),(R_ (No_omega^ y))) or ex b being Surreal st
( b in R_ (No_omega^ (x + y)) & b <= a ) )
set Nx = No_omega^ x;
set Ny = No_omega^ y;
assume a in comp ((L_ (No_omega^ x)),(No_omega^ x),(No_omega^ y),(R_ (No_omega^ y))) ; :: thesis: ex b being Surreal st
( b in R_ (No_omega^ (x + y)) & b <= a )
then consider x1, y1 being Surreal such that
A63: ( a = ((x1 * (No_omega^ y)) + ((No_omega^ x) * y1)) - (x1 * y1) & x1 in L_ (No_omega^ x) & y1 in R_ (No_omega^ y) ) by SURREALR:def 15;
A64: x + y = [(((L_ x) ++ {y}) \/ ({x} ++ (L_ y))),(((R_ x) ++ {y}) \/ ({x} ++ (R_ y)))] by SURREALR:28;
consider yL being Surreal, s being positive Real such that
A65: ( yL in R_ y & y1 = (No_omega^ yL) * (uReal . s) ) by A63, Th23;
yL in (L_ y) \/ (R_ y) by A65, XBOOLE_0:def 3;
then A66: (born x) (+) (born yL) in (born x) (+) (born y) by ORDINAL7:94, SURREALO:1;

per cases ( x1 = 0_No or x1 <> 0_No ) ;

suppose A67: x1 = 0_No ; :: thesis: ex b being Surreal st
( b in R_ (No_omega^ (x + y)) & b <= a )

( a == ((No_omega^ x) * (No_omega^ yL)) * (uReal . s) & ((No_omega^ x) * (No_omega^ yL)) * (uReal . s) == (No_omega^ (x + yL)) * (uReal . s) ) by A65, A63, A67, A66, A62, A2, SURREALR:69, SURREALR:54;
then A68: a == (No_omega^ (x + yL)) * (uReal . s) by SURREALO:9;
x in {x} by TARSKI:def 1;
then x + yL in {x} ++ (R_ y) by A65, SURREALR:def 8;
then x + yL in R_ (x + y) by A64, XBOOLE_0:def 3;
hence ex b being Surreal st
( b in R_ (No_omega^ (x + y)) & b <= a ) by A68, Th23; :: thesis: verum

end;

suppose x1 <> 0_No ; :: thesis: ex b being Surreal st
( b in R_ (No_omega^ (x + y)) & b <= a )

then consider xL being Surreal, r being positive Real such that
A69: ( xL in L_ x & x1 = (No_omega^ xL) * (uReal . r) ) by A63, Th22;
( (No_omega^ x) * y1 == ((No_omega^ x) * (No_omega^ yL)) * (uReal . s) & ((No_omega^ x) * (No_omega^ yL)) * (uReal . s) == (No_omega^ (x + yL)) * (uReal . s) ) by A65, A66, A62, A2, SURREALR:69, SURREALR:54;
then A70: (No_omega^ x) * y1 == (No_omega^ (x + yL)) * (uReal . s) by SURREALO:9;
x in {x} by TARSKI:def 1;
then x + yL in {x} ++ (R_ y) by A65, SURREALR:def 8;
then A71: x + yL in R_ (x + y) by A64, XBOOLE_0:def 3;
A72: 0_No <= y1 by A65, SURREALI:def 8;
A73: 0_No <= x1 * (No_omega^ y) by A69, SURREALI:def 8;
set H = uReal . (1 / 2);
(1 / 2) + (1 / 2) = 1 ;
then ( (((No_omega^ x) * y1) * (uReal . (1 / 2))) + (((No_omega^ x) * y1) * (uReal . (1 / 2))) == ((No_omega^ x) * y1) * ((uReal . (1 / 2)) + (uReal . (1 / 2))) & ((No_omega^ x) * y1) * ((uReal . (1 / 2)) + (uReal . (1 / 2))) == ((No_omega^ x) * y1) * 1_No & ((No_omega^ x) * y1) * 1_No = (No_omega^ x) * y1 ) by SURREALN:55, SURREALN:48, SURREALR:51, SURREALR:67;
then (((No_omega^ x) * y1) * (uReal . (1 / 2))) + (((No_omega^ x) * y1) * (uReal . (1 / 2))) == (No_omega^ x) * y1 by SURREALO:4;
then A74: (((uReal . (1 / 2)) * ((No_omega^ x) * y1)) + ((uReal . (1 / 2)) * ((No_omega^ x) * y1))) + (- (x1 * y1)) == ((No_omega^ x) * y1) + (- (x1 * y1)) by SURREALR:32;
( x in {x} & L_ x << {x} ) by TARSKI:def 1, SURREALO:11;
then No_omega^ xL infinitely< No_omega^ x by A69, Th25;
then x1 infinitely< No_omega^ x by A69, Th13;
then x1 infinitely< (uReal . (1 / 2)) * (No_omega^ x) by Th13;
then x1 <= (uReal . (1 / 2)) * (No_omega^ x) by Th9;
then ( x1 * y1 <= ((uReal . (1 / 2)) * (No_omega^ x)) * y1 & ((uReal . (1 / 2)) * (No_omega^ x)) * y1 == (uReal . (1 / 2)) * ((No_omega^ x) * y1) ) by A72, SURREALR:75, SURREALR:69;
then x1 * y1 <= (uReal . (1 / 2)) * ((No_omega^ x) * y1) by SURREALO:4;
then 0_No <= ((uReal . (1 / 2)) * ((No_omega^ x) * y1)) - (x1 * y1) by SURREALR:46;
then ( (uReal . (1 / 2)) * ((No_omega^ x) * y1) = 0_No + ((uReal . (1 / 2)) * ((No_omega^ x) * y1)) & 0_No + ((uReal . (1 / 2)) * ((No_omega^ x) * y1)) <= ((uReal . (1 / 2)) * ((No_omega^ x) * y1)) + (((uReal . (1 / 2)) * ((No_omega^ x) * y1)) - (x1 * y1)) & ((uReal . (1 / 2)) * ((No_omega^ x) * y1)) + (((uReal . (1 / 2)) * ((No_omega^ x) * y1)) - (x1 * y1)) = (((uReal . (1 / 2)) * ((No_omega^ x) * y1)) + ((uReal . (1 / 2)) * ((No_omega^ x) * y1))) + (- (x1 * y1)) ) by SURREALR:43, SURREALR:37;
then (uReal . (1 / 2)) * ((No_omega^ x) * y1) <= ((No_omega^ x) * y1) + (- (x1 * y1)) by A74, SURREALO:4;
then A75: ( (uReal . (1 / 2)) * ((No_omega^ x) * y1) = ((uReal . (1 / 2)) * ((No_omega^ x) * y1)) + 0_No & ((uReal . (1 / 2)) * ((No_omega^ x) * y1)) + 0_No <= (x1 * (No_omega^ y)) + (((No_omega^ x) * y1) + (- (x1 * y1))) & (x1 * (No_omega^ y)) + (((No_omega^ x) * y1) + (- (x1 * y1))) = a ) by A73, A63, SURREALR:43, SURREALR:37;
( (uReal . (1 / 2)) * ((No_omega^ x) * y1) == (uReal . (1 / 2)) * ((No_omega^ (x + yL)) * (uReal . s)) & (uReal . (1 / 2)) * ((No_omega^ (x + yL)) * (uReal . s)) == ((uReal . (1 / 2)) * (uReal . s)) * (No_omega^ (x + yL)) ) by A70, SURREALR:54, SURREALR:69;
then A76: (uReal . (1 / 2)) * ((No_omega^ x) * y1) == ((uReal . (1 / 2)) * (uReal . s)) * (No_omega^ (x + yL)) by SURREALO:4;
((uReal . (1 / 2)) * (uReal . s)) * (No_omega^ (x + yL)) == (uReal . ((1 / 2) * s)) * (No_omega^ (x + yL)) by SURREALR:54, SURREALN:57;
then (uReal . (1 / 2)) * ((No_omega^ x) * y1) == (uReal . ((1 / 2) * s)) * (No_omega^ (x + yL)) by A76, SURREALO:4;
then (uReal . ((1 / 2) * s)) * (No_omega^ (x + yL)) <= a by A75, SURREALO:4;
hence ex b being Surreal st
( b in R_ (No_omega^ (x + y)) & b <= a ) by A71, Th23; :: thesis: verum

end;

end;

end;

for a being Surreal st a in R_ ((No_omega^ x) * (No_omega^ y)) holds
ex b being Surreal st
( b in R_ (No_omega^ (x + y)) & b <= a )

proof

let a be Surreal; :: thesis: ( a in R_ ((No_omega^ x) * (No_omega^ y)) implies ex b being Surreal st
( b in R_ (No_omega^ (x + y)) & b <= a ) )
assume a in R_ ((No_omega^ x) * (No_omega^ y)) ; :: thesis: ex b being Surreal st
( b in R_ (No_omega^ (x + y)) & b <= a )

per cases then ( a in comp ((L_ (No_omega^ x)),(No_omega^ x),(No_omega^ y),(R_ (No_omega^ y))) or a in comp ((R_ (No_omega^ x)),(No_omega^ x),(No_omega^ y),(L_ (No_omega^ y))) ) by A4, XBOOLE_0:def 3;

suppose a in comp ((L_ (No_omega^ x)),(No_omega^ x),(No_omega^ y),(R_ (No_omega^ y))) ; :: thesis: ex b being Surreal st
( b in R_ (No_omega^ (x + y)) & b <= a )

hence ex b being Surreal st
( b in R_ (No_omega^ (x + y)) & b <= a ) by A61, A3; :: thesis: verum

end;

suppose a in comp ((R_ (No_omega^ x)),(No_omega^ x),(No_omega^ y),(L_ (No_omega^ y))) ; :: thesis: ex b being Surreal st
( b in R_ (No_omega^ (x + y)) & b <= a )

then a in comp ((L_ (No_omega^ y)),(No_omega^ y),(No_omega^ x),(R_ (No_omega^ x))) by SURREALR:53;
hence ex b being Surreal st
( b in R_ (No_omega^ (x + y)) & b <= a ) by A61, A3; :: thesis: verum

end;

end;

end;

hence (No_omega^ x) * (No_omega^ y) == No_omega^ (x + y) by A6, A37, SURREAL0:44, A48, A49; :: thesis: verum

end;

for D being Ordinal holds S₁[D] from ORDINAL1:sch 2(A1);
hence (No_omega^ x) * (No_omega^ y) == No_omega^ (x + y) ; :: thesis: verum