let x, y be Surreal; :: thesis:
set Bx = born x;
set By = born y;
set A = (born x) (+) (born y);
consider S being Function-yielding c=-monotone Sequence such that
A1: ( dom S = succ ((born x) (+) (born y)) & No_sum_op ((born x) (+) (born y)) = S . ((born x) (+) (born y)) ) and
A2: for B being Ordinal st B in succ ((born x) (+) (born y)) holds
ex SB being ManySortedSet of Triangle B st
( S . B = SB & ( for x being object st x in Triangle B holds
SB . x = [((union (rng (S | B))) .: ([:(L_ (L_ x)),{(R_ x)}:] \/ [:{(L_ x)},(L_ (R_ x)):])),((union (rng (S | B))) .: ([:(R_ (L_ x)),{(R_ x)}:] \/ [:{(L_ x)},(R_ (R_ x)):]))] ) ) by Def6;
consider SA being ManySortedSet of Triangle ((born x) (+) (born y)) such that
A3: S . ((born x) (+) (born y)) = SA and
A4: for x being object st x in Triangle ((born x) (+) (born y)) holds
SA . x = [((union (rng (S | ((born x) (+) (born y))))) .: ([:(L_ (x `1)),{(R_ x)}:] \/ [:{(L_ x)},(L_ (R_ x)):])),((union (rng (S | ((born x) (+) (born y))))) .: ([:(R_ (L_ x)),{(R_ x)}:] \/ [:{(L_ x)},(R_ (R_ x)):]))] by A2, ORDINAL1:6;
set U = union (rng (S | ((born x) (+) (born y))));
A5: [x,y] in Triangle ((born x) (+) (born y)) by Def5;
( [x,y] `1 = x & [x,y] `2 = y ) ;
then A6: x + y = [((union (rng (S | ((born x) (+) (born y))))) .: ([:(L_ x),{y}:] \/ [:{x},(L_ y):])),((union (rng (S | ((born x) (+) (born y))))) .: ([:(R_ x),{y}:] \/ [:{x},(R_ y):]))] by A1, A3, A5, A4;
A7: (union (rng (S | ((born x) (+) (born y))))) .: [:(L_ x),{y}:] c= (L_ x) ++ {y}

proof

let a be object ; :: according to TARSKI:def 3 :: thesis:
assume a in (union (rng (S | ((born x) (+) (born y))))) .: [:(L_ x),{y}:] ; :: thesis:
then consider b being object such that
A8: ( b in dom (union (rng (S | ((born x) (+) (born y))))) & b in [:(L_ x),{y}:] & (union (rng (S | ((born x) (+) (born y))))) . b = a ) by FUNCT_1:def 6;
consider x1, y1 being object such that
A9: ( x1 in L_ x & y1 in {y} & b = [x1,y1] ) by ZFMISC_1:def 2, A8;
reconsider x1 = x1, y1 = y1 as Surreal by A9, SURREAL0:def 16;
set X1 = born x1;
set C = (born x1) (+) (born y);
x1 in (L_ x) \/ (R_ x) by A9, XBOOLE_0:def 3;
then A10: (born x1) (+) (born y) in (born x) (+) (born y) by SURREALO:1, ORDINAL7:94;
then A11: (born x1) (+) (born y) in succ ((born x) (+) (born y)) by ORDINAL1:8;
then consider SC being ManySortedSet of Triangle ((born x1) (+) (born y)) such that
A12: S . ((born x1) (+) (born y)) = SC and
for x being object st x in Triangle ((born x1) (+) (born y)) holds
SC . x = [((union (rng (S | ((born x1) (+) (born y))))) .: ([:(L_ (L_ x)),{(R_ x)}:] \/ [:{(L_ x)},(L_ (R_ x)):])),((union (rng (S | ((born x1) (+) (born y))))) .: ([:(R_ (L_ x)),{(R_ x)}:] \/ [:{(L_ x)},(R_ (R_ x)):]))] by A2;
A13: y = y1 by A9, TARSKI:def 1;
A14: dom SC = Triangle ((born x1) (+) (born y)) by PARTFUN1:def 2;
A15: [x1,y] in Triangle ((born x1) (+) (born y)) by Def5;
A16: x1 + y = SC . [x1,y] by A11, A1, A2, A12, Th26;
A17: SC . [x1,y] = (union (rng S)) . [x1,y] by A11, A14, A15, Th2, A1, A12;
(union (rng (S | ((born x) (+) (born y))))) . b = (union (rng S)) . b by A12, Th5, A10, A13, A9, A15, A14;
hence a in (L_ x) ++ {y} by A9, Def8, A8, A17, A16, A13; :: thesis:

end;

(L_ x) ++ {y} c= (union (rng (S | ((born x) (+) (born y))))) .: [:(L_ x),{y}:]

proof

let b be object ; :: according to TARSKI:def 3 :: thesis:
assume b in (L_ x) ++ {y} ; :: thesis:
then consider x1, y1 being Surreal such that
A18: ( x1 in L_ x & y1 in {y} & b = x1 + y1 ) by Def8;
A19: y = y1 by A18, TARSKI:def 1;
set X1 = born x1;
set C = (born x1) (+) (born y);
x1 in (L_ x) \/ (R_ x) by A18, XBOOLE_0:def 3;
then A20: (born x1) (+) (born y) in (born x) (+) (born y) by SURREALO:1, ORDINAL7:94;
then A21: (born x1) (+) (born y) in succ ((born x) (+) (born y)) by ORDINAL1:8;
then consider SC being ManySortedSet of Triangle ((born x1) (+) (born y)) such that
A22: S . ((born x1) (+) (born y)) = SC and
for x being object st x in Triangle ((born x1) (+) (born y)) holds
SC . x = [((union (rng (S | ((born x1) (+) (born y))))) .: ([:(L_ (L_ x)),{(R_ x)}:] \/ [:{(L_ x)},(L_ (R_ x)):])),((union (rng (S | ((born x1) (+) (born y))))) .: ([:(R_ (L_ x)),{(R_ x)}:] \/ [:{(L_ x)},(R_ (R_ x)):]))] by A2;
A23: dom SC = Triangle ((born x1) (+) (born y)) by PARTFUN1:def 2;
A24: [x1,y] in Triangle ((born x1) (+) (born y)) by Def5;
A25: x1 + y = SC . [x1,y] by A21, A1, A2, A22, Th26;
SC . [x1,y] = (union (rng S)) . [x1,y] by A21, A23, A24, Th2, A1, A22;
then A26: (union (rng (S | ((born x) (+) (born y))))) . [x1,y] = b by A25, A18, A19, A22, Th5, A20, A24, A23;
A27: [x1,y] in dom (union (rng (S | ((born x) (+) (born y))))) by A22, Th5, A20, A24, A23;
[x1,y] in [:(L_ x),{y}:] by A18, A19, ZFMISC_1:87;
hence b in (union (rng (S | ((born x) (+) (born y))))) .: [:(L_ x),{y}:] by A26, A27, FUNCT_1:def 6; :: thesis:

end;

then A28: (union (rng (S | ((born x) (+) (born y))))) .: [:(L_ x),{y}:] = (L_ x) ++ {y} by A7, XBOOLE_0:def 10;
A29: (union (rng (S | ((born x) (+) (born y))))) .: [:(R_ x),{y}:] c= (R_ x) ++ {y}

proof

let a be object ; :: according to TARSKI:def 3 :: thesis:
assume a in (union (rng (S | ((born x) (+) (born y))))) .: [:(R_ x),{y}:] ; :: thesis:
then consider b being object such that
A30: ( b in dom (union (rng (S | ((born x) (+) (born y))))) & b in [:(R_ x),{y}:] & (union (rng (S | ((born x) (+) (born y))))) . b = a ) by FUNCT_1:def 6;
consider x1, y1 being object such that
A31: ( x1 in R_ x & y1 in {y} & b = [x1,y1] ) by ZFMISC_1:def 2, A30;
reconsider x1 = x1, y1 = y1 as Surreal by A31, SURREAL0:def 16;
set X1 = born x1;
set C = (born x1) (+) (born y);
x1 in (L_ x) \/ (R_ x) by A31, XBOOLE_0:def 3;
then A32: (born x1) (+) (born y) in (born x) (+) (born y) by SURREALO:1, ORDINAL7:94;
then A33: (born x1) (+) (born y) in succ ((born x) (+) (born y)) by ORDINAL1:8;
then consider SC being ManySortedSet of Triangle ((born x1) (+) (born y)) such that
A34: S . ((born x1) (+) (born y)) = SC and
for x being object st x in Triangle ((born x1) (+) (born y)) holds
SC . x = [((union (rng (S | ((born x1) (+) (born y))))) .: ([:(L_ (L_ x)),{(R_ x)}:] \/ [:{(L_ x)},(L_ (R_ x)):])),((union (rng (S | ((born x1) (+) (born y))))) .: ([:(R_ (L_ x)),{(R_ x)}:] \/ [:{(L_ x)},(R_ (R_ x)):]))] by A2;
A35: y = y1 by A31, TARSKI:def 1;
A36: dom SC = Triangle ((born x1) (+) (born y)) by PARTFUN1:def 2;
A37: [x1,y] in Triangle ((born x1) (+) (born y)) by Def5;
A38: x1 + y = SC . [x1,y] by A33, A1, A2, A34, Th26;
A39: SC . [x1,y] = (union (rng S)) . [x1,y] by A33, A36, A37, Th2, A1, A34;
(union (rng (S | ((born x) (+) (born y))))) . b = (union (rng S)) . b by A34, Th5, A32, A35, A31, A37, A36;
hence a in (R_ x) ++ {y} by A31, Def8, A30, A39, A38, A35; :: thesis:

end;

(R_ x) ++ {y} c= (union (rng (S | ((born x) (+) (born y))))) .: [:(R_ x),{y}:]

proof

let b be object ; :: according to TARSKI:def 3 :: thesis:
assume b in (R_ x) ++ {y} ; :: thesis:
then consider x1, y1 being Surreal such that
A40: ( x1 in R_ x & y1 in {y} & b = x1 + y1 ) by Def8;
A41: y = y1 by A40, TARSKI:def 1;
set X1 = born x1;
set C = (born x1) (+) (born y);
x1 in (L_ x) \/ (R_ x) by A40, XBOOLE_0:def 3;
then A42: (born x1) (+) (born y) in (born x) (+) (born y) by SURREALO:1, ORDINAL7:94;
then A43: (born x1) (+) (born y) in succ ((born x) (+) (born y)) by ORDINAL1:8;
then consider SC being ManySortedSet of Triangle ((born x1) (+) (born y)) such that
A44: S . ((born x1) (+) (born y)) = SC and
for x being object st x in Triangle ((born x1) (+) (born y)) holds
SC . x = [((union (rng (S | ((born x1) (+) (born y))))) .: ([:(L_ (L_ x)),{(R_ x)}:] \/ [:{(L_ x)},(L_ (R_ x)):])),((union (rng (S | ((born x1) (+) (born y))))) .: ([:(R_ (L_ x)),{(R_ x)}:] \/ [:{(L_ x)},(R_ (R_ x)):]))] by A2;
A45: dom SC = Triangle ((born x1) (+) (born y)) by PARTFUN1:def 2;
A46: [x1,y] in Triangle ((born x1) (+) (born y)) by Def5;
A47: x1 + y = SC . [x1,y] by A43, A1, A2, A44, Th26;
SC . [x1,y] = (union (rng S)) . [x1,y] by A43, A45, A46, Th2, A1, A44;
then A48: (union (rng (S | ((born x) (+) (born y))))) . [x1,y] = b by A47, A44, Th5, A42, A46, A45, A40, A41;
A49: [x1,y] in dom (union (rng (S | ((born x) (+) (born y))))) by A44, Th5, A42, A46, A45;
[x1,y] in [:(R_ x),{y}:] by A40, A41, ZFMISC_1:87;
hence b in (union (rng (S | ((born x) (+) (born y))))) .: [:(R_ x),{y}:] by A48, A49, FUNCT_1:def 6; :: thesis:

end;

then A50: (union (rng (S | ((born x) (+) (born y))))) .: [:(R_ x),{y}:] = (R_ x) ++ {y} by A29, XBOOLE_0:def 10;
A51: (union (rng (S | ((born x) (+) (born y))))) .: [:{x},(L_ y):] c= {x} ++ (L_ y)

proof

let a be object ; :: according to TARSKI:def 3 :: thesis:
assume a in (union (rng (S | ((born x) (+) (born y))))) .: [:{x},(L_ y):] ; :: thesis:
then consider b being object such that
A52: ( b in dom (union (rng (S | ((born x) (+) (born y))))) & b in [:{x},(L_ y):] & (union (rng (S | ((born x) (+) (born y))))) . b = a ) by FUNCT_1:def 6;
consider x1, y1 being object such that
A53: ( x1 in {x} & y1 in L_ y & b = [x1,y1] ) by ZFMISC_1:def 2, A52;
reconsider x1 = x1, y1 = y1 as Surreal by A53, SURREAL0:def 16;
set Y1 = born y1;
set C = (born x) (+) (born y1);
y1 in (L_ y) \/ (R_ y) by A53, XBOOLE_0:def 3;
then A54: (born x) (+) (born y1) in (born x) (+) (born y) by SURREALO:1, ORDINAL7:94;
then A55: (born x) (+) (born y1) in succ ((born x) (+) (born y)) by ORDINAL1:8;
then consider SC being ManySortedSet of Triangle ((born x) (+) (born y1)) such that
A56: S . ((born x) (+) (born y1)) = SC and
for x being object st x in Triangle ((born x) (+) (born y1)) holds
SC . x = [((union (rng (S | ((born x) (+) (born y1))))) .: ([:(L_ (L_ x)),{(R_ x)}:] \/ [:{(L_ x)},(L_ (R_ x)):])),((union (rng (S | ((born x) (+) (born y1))))) .: ([:(R_ (L_ x)),{(R_ x)}:] \/ [:{(L_ x)},(R_ (R_ x)):]))] by A2;
A57: x = x1 by A53, TARSKI:def 1;
A58: dom SC = Triangle ((born x) (+) (born y1)) by PARTFUN1:def 2;
A59: [x,y1] in Triangle ((born x) (+) (born y1)) by Def5;
A60: x + y1 = SC . [x,y1] by A55, A1, A2, A56, Th26;
A61: SC . [x,y1] = (union (rng S)) . [x,y1] by A55, A58, A59, Th2, A1, A56;
(union (rng (S | ((born x) (+) (born y))))) . b = (union (rng S)) . b by A56, Th5, A54, A57, A53, A59, A58;
hence a in {x} ++ (L_ y) by A53, Def8, A52, A61, A60, A57; :: thesis:

end;

{x} ++ (L_ y) c= (union (rng (S | ((born x) (+) (born y))))) .: [:{x},(L_ y):]

proof

let b be object ; :: according to TARSKI:def 3 :: thesis:
assume b in {x} ++ (L_ y) ; :: thesis:
then consider x1, y1 being Surreal such that
A62: ( x1 in {x} & y1 in L_ y & b = x1 + y1 ) by Def8;
A63: x = x1 by A62, TARSKI:def 1;
set Y1 = born y1;
set C = (born x) (+) (born y1);
y1 in (L_ y) \/ (R_ y) by A62, XBOOLE_0:def 3;
then A64: (born x) (+) (born y1) in (born x) (+) (born y) by SURREALO:1, ORDINAL7:94;
then A65: (born x) (+) (born y1) in succ ((born x) (+) (born y)) by ORDINAL1:8;
then consider SC being ManySortedSet of Triangle ((born x) (+) (born y1)) such that
A66: S . ((born x) (+) (born y1)) = SC and
for x being object st x in Triangle ((born x) (+) (born y1)) holds
SC . x = [((union (rng (S | ((born x) (+) (born y1))))) .: ([:(L_ (L_ x)),{(R_ x)}:] \/ [:{(L_ x)},(L_ (R_ x)):])),((union (rng (S | ((born x) (+) (born y1))))) .: ([:(R_ (L_ x)),{(R_ x)}:] \/ [:{(L_ x)},(R_ (R_ x)):]))] by A2;
A67: dom SC = Triangle ((born x) (+) (born y1)) by PARTFUN1:def 2;
A68: [x,y1] in Triangle ((born x) (+) (born y1)) by Def5;
A69: x + y1 = SC . [x,y1] by A65, A1, A2, A66, Th26;
SC . [x,y1] = (union (rng S)) . [x,y1] by A65, A67, A68, Th2, A1, A66;
then A70: (union (rng (S | ((born x) (+) (born y))))) . [x,y1] = b by A69, A66, Th5, A64, A68, A67, A62, A63;
A71: [x,y1] in dom (union (rng (S | ((born x) (+) (born y))))) by A66, Th5, A64, A68, A67;
[x,y1] in [:{x},(L_ y):] by A62, A63, ZFMISC_1:87;
hence b in (union (rng (S | ((born x) (+) (born y))))) .: [:{x},(L_ y):] by A70, A71, FUNCT_1:def 6; :: thesis:

end;

then A72: {x} ++ (L_ y) = (union (rng (S | ((born x) (+) (born y))))) .: [:{x},(L_ y):] by A51, XBOOLE_0:def 10;
A73: (union (rng (S | ((born x) (+) (born y))))) .: [:{x},(R_ y):] c= {x} ++ (R_ y)

proof

let a be object ; :: according to TARSKI:def 3 :: thesis:
assume a in (union (rng (S | ((born x) (+) (born y))))) .: [:{x},(R_ y):] ; :: thesis:
then consider b being object such that
A74: ( b in dom (union (rng (S | ((born x) (+) (born y))))) & b in [:{x},(R_ y):] & (union (rng (S | ((born x) (+) (born y))))) . b = a ) by FUNCT_1:def 6;
consider x1, y1 being object such that
A75: ( x1 in {x} & y1 in R_ y & b = [x1,y1] ) by ZFMISC_1:def 2, A74;
reconsider x1 = x1, y1 = y1 as Surreal by A75, SURREAL0:def 16;
set Y1 = born y1;
set C = (born x) (+) (born y1);
y1 in (L_ y) \/ (R_ y) by A75, XBOOLE_0:def 3;
then A76: (born x) (+) (born y1) in (born x) (+) (born y) by SURREALO:1, ORDINAL7:94;
then A77: (born x) (+) (born y1) in succ ((born x) (+) (born y)) by ORDINAL1:8;
then consider SC being ManySortedSet of Triangle ((born x) (+) (born y1)) such that
A78: S . ((born x) (+) (born y1)) = SC and
for x being object st x in Triangle ((born x) (+) (born y1)) holds
SC . x = [((union (rng (S | ((born x) (+) (born y1))))) .: ([:(L_ (L_ x)),{(R_ x)}:] \/ [:{(L_ x)},(L_ (R_ x)):])),((union (rng (S | ((born x) (+) (born y1))))) .: ([:(R_ (L_ x)),{(R_ x)}:] \/ [:{(L_ x)},(R_ (R_ x)):]))] by A2;
A79: x = x1 by A75, TARSKI:def 1;
A80: dom SC = Triangle ((born x) (+) (born y1)) by PARTFUN1:def 2;
A81: [x,y1] in Triangle ((born x) (+) (born y1)) by Def5;
A82: x + y1 = SC . [x,y1] by A77, A1, A2, A78, Th26;
A83: SC . [x,y1] = (union (rng S)) . [x,y1] by A77, A80, A81, Th2, A1, A78;
(union (rng (S | ((born x) (+) (born y))))) . b = (union (rng S)) . b by A78, Th5, A76, A79, A75, A81, A80;
hence a in {x} ++ (R_ y) by A75, Def8, A74, A83, A82, A79; :: thesis:

end;

{x} ++ (R_ y) c= (union (rng (S | ((born x) (+) (born y))))) .: [:{x},(R_ y):]

proof

let b be object ; :: according to TARSKI:def 3 :: thesis:
assume b in {x} ++ (R_ y) ; :: thesis:
then consider x1, y1 being Surreal such that
A84: ( x1 in {x} & y1 in R_ y & b = x1 + y1 ) by Def8;
A85: x = x1 by A84, TARSKI:def 1;
set Y1 = born y1;
set C = (born x) (+) (born y1);
y1 in (L_ y) \/ (R_ y) by A84, XBOOLE_0:def 3;
then A86: (born x) (+) (born y1) in (born x) (+) (born y) by SURREALO:1, ORDINAL7:94;
then A87: (born x) (+) (born y1) in succ ((born x) (+) (born y)) by ORDINAL1:8;
then consider SC being ManySortedSet of Triangle ((born x) (+) (born y1)) such that
A88: S . ((born x) (+) (born y1)) = SC and
for x being object st x in Triangle ((born x) (+) (born y1)) holds
SC . x = [((union (rng (S | ((born x) (+) (born y1))))) .: ([:(L_ (L_ x)),{(R_ x)}:] \/ [:{(L_ x)},(L_ (R_ x)):])),((union (rng (S | ((born x) (+) (born y1))))) .: ([:(R_ (L_ x)),{(R_ x)}:] \/ [:{(L_ x)},(R_ (R_ x)):]))] by A2;
A89: dom SC = Triangle ((born x) (+) (born y1)) by PARTFUN1:def 2;
A90: [x,y1] in Triangle ((born x) (+) (born y1)) by Def5;
A91: x + y1 = SC . [x,y1] by A87, A1, A2, A88, Th26;
SC . [x,y1] = (union (rng S)) . [x,y1] by A87, A89, A90, Th2, A1, A88;
then A92: (union (rng (S | ((born x) (+) (born y))))) . [x,y1] = b by A91, A88, Th5, A86, A90, A89, A84, A85;
A93: [x,y1] in dom (union (rng (S | ((born x) (+) (born y))))) by A88, Th5, A86, A90, A89;
[x,y1] in [:{x},(R_ y):] by A84, A85, ZFMISC_1:87;
hence b in (union (rng (S | ((born x) (+) (born y))))) .: [:{x},(R_ y):] by A92, A93, FUNCT_1:def 6; :: thesis:

end;

then A94: {x} ++ (R_ y) = (union (rng (S | ((born x) (+) (born y))))) .: [:{x},(R_ y):] by A73, XBOOLE_0:def 10;
(union (rng (S | ((born x) (+) (born y))))) .: ([:(L_ x),{y}:] \/ [:{x},(L_ y):]) = ((L_ x) ++ {y}) \/ ({x} ++ (L_ y)) by A28, A72, RELAT_1:120;
hence x + y = [(((L_ x) ++ {y}) \/ ({x} ++ (L_ y))),(((R_ x) ++ {y}) \/ ({x} ++ (R_ y)))] by A6, A50, A94, RELAT_1:120; :: thesis: