let x, y, z be Surreal; :: thesis: x * (y + z) == (x * y) + (x * z)
defpred S₁[ Ordinal] means for x, y, z being Surreal st ((born x) (+) (born y)) (+) (born z) c= $1 holds
x * (y + z) == (x * y) + (x * z);
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, z be Surreal; :: thesis: ( ((born x) (+) (born y)) (+) (born z) c= D implies x * (y + z) == (x * y) + (x * z) )
assume A3: ((born x) (+) (born y)) (+) (born z) c= D ; :: thesis: x * (y + z) == (x * y) + (x * z)
set xy = x * y;
set xz = x * z;
set yz = y + z;
A4: x * y = [((comp ((L_ x),x,y,(L_ y))) \/ (comp ((R_ x),x,y,(R_ y)))),((comp ((L_ x),x,y,(R_ y))) \/ (comp ((R_ x),x,y,(L_ y))))] by Th50;
A5: x * z = [((comp ((L_ x),x,z,(L_ z))) \/ (comp ((R_ x),x,z,(R_ z)))),((comp ((L_ x),x,z,(R_ z))) \/ (comp ((R_ x),x,z,(L_ z))))] by Th50;
A6: y + z = [(((L_ y) ++ {z}) \/ ({y} ++ (L_ z))),(((R_ y) ++ {z}) \/ ({y} ++ (R_ z)))] by Th28;
A7: x * (y + z) = [((comp ((L_ x),x,(y + z),(L_ (y + z)))) \/ (comp ((R_ x),x,(y + z),(R_ (y + z))))),((comp ((L_ x),x,(y + z),(R_ (y + z)))) \/ (comp ((R_ x),x,(y + z),(L_ (y + z)))))] by Th50;
A8: (x * y) + (x * z) = [(((L_ (x * y)) ++ {(x * z)}) \/ ({(x * y)} ++ (L_ (x * z)))),(((R_ (x * y)) ++ {(x * z)}) \/ ({(x * y)} ++ (R_ (x * z))))] by Th28;
A9: comp ((L_ x),x,(y + z),(L_ (y + z))) = (comp ((L_ x),x,(y + z),((L_ y) ++ {z}))) \/ (comp ((L_ x),x,(y + z),({y} ++ (L_ z)))) by A6, Th60;
A10: comp ((R_ x),x,(y + z),(L_ (y + z))) = (comp ((R_ x),x,(y + z),((L_ y) ++ {z}))) \/ (comp ((R_ x),x,(y + z),({y} ++ (L_ z)))) by A6, Th60;
A11: comp ((R_ x),x,(y + z),(R_ (y + z))) = (comp ((R_ x),x,(y + z),((R_ y) ++ {z}))) \/ (comp ((R_ x),x,(y + z),({y} ++ (R_ z)))) by A6, Th60;
A12: comp ((L_ x),x,(y + z),(R_ (y + z))) = (comp ((L_ x),x,(y + z),((R_ y) ++ {z}))) \/ (comp ((L_ x),x,(y + z),({y} ++ (R_ z)))) by A6, Th60;
A13: for X, Z being surreal-membered set st ( X = L_ x or X = R_ x ) & ( Z = L_ z or Z = R_ z ) holds
(comp (X,x,z,Z)) ++ {(x * y)} <==> comp (X,x,(y + z),(Z ++ {y}))

proof

let X, Z be surreal-membered set ; :: thesis: ( ( X = L_ x or X = R_ x ) & ( Z = L_ z or Z = R_ z ) implies (comp (X,x,z,Z)) ++ {(x * y)} <==> comp (X,x,(y + z),(Z ++ {y})) )
assume A14: ( ( X = L_ x or X = R_ x ) & ( Z = L_ z or Z = R_ z ) ) ; :: thesis: (comp (X,x,z,Z)) ++ {(x * y)} <==> comp (X,x,(y + z),(Z ++ {y}))
for o being Surreal st o in (comp (X,x,z,Z)) ++ {(x * y)} holds
ex b being Surreal st
( b in comp (X,x,(y + z),(Z ++ {y})) & o == b )

proof

let o be Surreal; :: thesis: ( o in (comp (X,x,z,Z)) ++ {(x * y)} implies ex b being Surreal st
( b in comp (X,x,(y + z),(Z ++ {y})) & o == b ) )
assume o in (comp (X,x,z,Z)) ++ {(x * y)} ; :: thesis: ex b being Surreal st
( b in comp (X,x,(y + z),(Z ++ {y})) & o == b )
then consider xz1, xy1 being Surreal such that
A15: ( xz1 in comp (X,x,z,Z) & xy1 in {(x * y)} & o = xz1 + xy1 ) by Def8;
consider x1, z1 being Surreal such that
A16: ( xz1 = ((x1 * z) + (x * z1)) - (x1 * z1) & x1 in X & z1 in Z ) by A15, Def15;
A17: ( R_ x <> {x} & {x} <> L_ x & R_ z <> {z} & {z} <> L_ z ) by SURREALO:2;
A18: ( x in {x} & y in {y} & z in {z} ) by TARSKI:def 1;
((born x1) (+) (born y)) (+) (born z) in ((born x) (+) (born y)) (+) (born z) by A14, A16, A18, A17, Lm7;
then A19: x1 * (y + z) == (x1 * y) + (x1 * z) by A2, A3;
set yz1 = y + z1;
((born x) (+) (born y)) (+) (born z1) in ((born x) (+) (born y)) (+) (born z) by A14, A18, A17, Lm7, A16;
then A20: x * (y + z1) == (x * y) + (x * z1) by A2, A3;
A21: ((born x1) (+) (born y)) (+) (born z1) in ((born x) (+) (born y)) (+) (born z) by A14, A18, A17, Lm7, A16;
A22: - ((x1 * z1) + (x1 * y)) = (- (x1 * z1)) + (- (x1 * y)) by Th40;
y + z1 in {y} ++ Z by A18, A16, Def8;
then A23: ((x1 * (y + z)) + (x * (y + z1))) - (x1 * (y + z1)) in comp (X,x,(y + z),({y} ++ Z)) by A16, Def15;
(x1 * z) + ((x * y) + (x * z1)) = ((x1 * z) + (x * z1)) + (x * y) by Th37;
then A24: ((x1 * z) + ((x * y) + (x * z1))) + (- (x1 * z1)) = (x * y) + (((x1 * z) + (x * z1)) + (- (x1 * z1))) by Th37;
A25: (x1 * y) - (x1 * y) == 0_No by Th39;
A26: - (x1 * (y + z1)) == (- (x1 * z1)) + (- (x1 * y)) by A22, A21, A2, A3, Th65;
(x1 * (y + z)) + (x * (y + z1)) == ((x1 * y) + (x1 * z)) + ((x * y) + (x * z1)) by A19, A20, Th43;
then A27: ((x1 * (y + z)) + (x * (y + z1))) + (- (x1 * (y + z1))) == (((x1 * y) + (x1 * z)) + ((x * y) + (x * z1))) + ((- (x1 * z1)) + (- (x1 * y))) by A26, Th43;
(((x1 * y) + (x1 * z)) + ((x * y) + (x * z1))) + ((- (x1 * z1)) + (- (x1 * y))) = ((x1 * y) + ((x1 * z) + ((x * y) + (x * z1)))) + ((- (x1 * z1)) + (- (x1 * y))) by Th37
.= (((x1 * y) + ((x1 * z) + ((x * y) + (x * z1)))) + (- (x1 * z1))) + (- (x1 * y)) by Th37
.= ((x1 * y) + (((x1 * z) + ((x * y) + (x * z1))) + (- (x1 * z1)))) + (- (x1 * y)) by Th37
.= ((x1 * y) + (- (x1 * y))) + ((((x1 * z) + (x * z1)) + (- (x1 * z1))) + (x * y)) by A24, Th37 ;
then ( ((x1 * (y + z)) + (x * (y + z1))) + (- (x1 * (y + z1))) == ((x1 * y) + (- (x1 * y))) + o & ((x1 * y) + (- (x1 * y))) + o == 0_No + o & 0_No + o = o ) by A27, A16, A15, TARSKI:def 1, A25, Th43;
hence ex b being Surreal st
( b in comp (X,x,(y + z),(Z ++ {y})) & o == b ) by A23, SURREALO:10; :: thesis: verum

end;

hence (comp (X,x,z,Z)) ++ {(x * y)} <=_ comp (X,x,(y + z),(Z ++ {y})) by Th61; :: according to SURREALO:def 4 :: thesis: comp (X,x,(y + z),(Z ++ {y})) <=_ (comp (X,x,z,Z)) ++ {(x * y)}
for o being Surreal st o in comp (X,x,(y + z),(Z ++ {y})) holds
ex b being Surreal st
( b in (comp (X,x,z,Z)) ++ {(x * y)} & o == b )

proof

let o be Surreal; :: thesis: ( o in comp (X,x,(y + z),(Z ++ {y})) implies ex b being Surreal st
( b in (comp (X,x,z,Z)) ++ {(x * y)} & o == b ) )
assume o in comp (X,x,(y + z),(Z ++ {y})) ; :: thesis: ex b being Surreal st
( b in (comp (X,x,z,Z)) ++ {(x * y)} & o == b )
then consider x1, yz1 being Surreal such that
A28: ( o = ((x1 * (y + z)) + (x * yz1)) - (x1 * yz1) & x1 in X & yz1 in Z ++ {y} ) by Def15;
consider z1, y1 being Surreal such that
A29: ( z1 in Z & y1 in {y} & yz1 = z1 + y1 ) by A28, Def8;
A30: y1 = y by A29, TARSKI:def 1;
A31: ( R_ x <> {x} & {x} <> L_ x & R_ z <> {z} & {z} <> L_ z ) by SURREALO:2;
A32: ( x in {x} & y in {y} & z in {z} ) by TARSKI:def 1;
((born x1) (+) (born y)) (+) (born z) in ((born x) (+) (born y)) (+) (born z) by A14, A32, A31, A28, Lm7;
then A33: x1 * (y + z) == (x1 * y) + (x1 * z) by A2, A3;
((born x) (+) (born y1)) (+) (born z1) in ((born x) (+) (born y)) (+) (born z) by A14, A32, A31, Lm7, A29;
then A34: x * yz1 == (x * y) + (x * z1) by A2, A3, A29, A30;
((born x1) (+) (born y1)) (+) (born z1) in ((born x) (+) (born y)) (+) (born z) by A14, A31, A28, Lm7, A29;
then A35: x1 * yz1 == (x1 * z1) + (x1 * y) by A2, A3, A29, A30;
A36: ((x1 * z) + (x * z1)) - (x1 * z1) in comp (X,x,z,Z) by A28, A29, Def15;
x * y in {(x * y)} by TARSKI:def 1;
then A37: (((x1 * z) + (x * z1)) + (- (x1 * z1))) + (x * y) in (comp (X,x,z,Z)) ++ {(x * y)} by A36, Def8;
(x1 * y) - (x1 * y) == 0_No by Th39;
then A38: ((x1 * y) + (- (x1 * y))) + ((((x1 * z) + (x * z1)) + (- (x1 * z1))) + (x * y)) == 0_No + ((((x1 * z) + (x * z1)) + (- (x1 * z1))) + (x * y)) by Th43;
(x1 * z) + ((x * y) + (x * z1)) = ((x1 * z) + (x * z1)) + (x * y) by Th37;
then A39: ((x1 * z) + ((x * y) + (x * z1))) + (- (x1 * z1)) = (x * y) + (((x1 * z) + (x * z1)) + (- (x1 * z1))) by Th37;
- (x1 * yz1) == - ((x1 * z1) + (x1 * y)) by A35, Th10;
then A40: - (x1 * yz1) == (- (x1 * z1)) + (- (x1 * y)) by Th40;
(x1 * (y + z)) + (x * yz1) == ((x1 * y) + (x1 * z)) + ((x * y) + (x * z1)) by A33, A34, Th43;
then A41: o == (((x1 * y) + (x1 * z)) + ((x * y) + (x * z1))) + ((- (x1 * z1)) + (- (x1 * y))) by A40, A28, Th43;
(((x1 * y) + (x1 * z)) + ((x * y) + (x * z1))) + ((- (x1 * z1)) + (- (x1 * y))) = ((x1 * y) + ((x1 * z) + ((x * y) + (x * z1)))) + ((- (x1 * z1)) + (- (x1 * y))) by Th37
.= (((x1 * y) + ((x1 * z) + ((x * y) + (x * z1)))) + (- (x1 * z1))) + (- (x1 * y)) by Th37
.= ((x1 * y) + (((x1 * z) + ((x * y) + (x * z1))) + (- (x1 * z1)))) + (- (x1 * y)) by Th37
.= ((x1 * y) + (- (x1 * y))) + ((((x1 * z) + (x * z1)) + (- (x1 * z1))) + (x * y)) by A39, Th37 ;
then o == 0_No + ((((x1 * z) + (x * z1)) + (- (x1 * z1))) + (x * y)) by A41, A38, SURREALO:4;
hence ex b being Surreal st
( b in (comp (X,x,z,Z)) ++ {(x * y)} & o == b ) by A37; :: thesis: verum

end;

hence comp (X,x,(y + z),(Z ++ {y})) <=_ (comp (X,x,z,Z)) ++ {(x * y)} by Th61; :: thesis: verum

end;

A42: for X, Y being surreal-membered set st ( X = L_ x or X = R_ x ) & ( Y = L_ y or Y = R_ y ) holds
(comp (X,x,y,Y)) ++ {(x * z)} <==> comp (X,x,(y + z),(Y ++ {z}))

proof

let X, Y be surreal-membered set ; :: thesis: ( ( X = L_ x or X = R_ x ) & ( Y = L_ y or Y = R_ y ) implies (comp (X,x,y,Y)) ++ {(x * z)} <==> comp (X,x,(y + z),(Y ++ {z})) )
assume A43: ( ( X = L_ x or X = R_ x ) & ( Y = L_ y or Y = R_ y ) ) ; :: thesis: (comp (X,x,y,Y)) ++ {(x * z)} <==> comp (X,x,(y + z),(Y ++ {z}))
for o being Surreal st o in (comp (X,x,y,Y)) ++ {(x * z)} holds
ex b being Surreal st
( b in comp (X,x,(y + z),(Y ++ {z})) & o == b )

proof

let o be Surreal; :: thesis: ( o in (comp (X,x,y,Y)) ++ {(x * z)} implies ex b being Surreal st
( b in comp (X,x,(y + z),(Y ++ {z})) & o == b ) )
assume o in (comp (X,x,y,Y)) ++ {(x * z)} ; :: thesis: ex b being Surreal st
( b in comp (X,x,(y + z),(Y ++ {z})) & o == b )
then consider xy1, xz1 being Surreal such that
A44: ( xy1 in comp (X,x,y,Y) & xz1 in {(x * z)} & o = xy1 + xz1 ) by Def8;
consider x1, y1 being Surreal such that
A45: ( xy1 = ((x1 * y) + (x * y1)) - (x1 * y1) & x1 in X & y1 in Y ) by A44, Def15;
A46: xz1 = x * z by A44, TARSKI:def 1;
A47: ((x1 * y) + (x1 * z)) + ((x * y1) + (x * z)) = (x1 * y) + ((x1 * z) + ((x * z) + (x * y1))) by Th37
.= (x1 * y) + (((x1 * z) + (x * z)) + (x * y1)) by Th37
.= ((x1 * y) + (x * y1)) + ((x1 * z) + (x * z)) by Th37 ;
A48: ( R_ x <> {x} & {x} <> L_ x & R_ y <> {y} & {y} <> L_ y ) by SURREALO:2;
A49: ( x in {x} & y in {y} & z in {z} ) by TARSKI:def 1;
((born x1) (+) (born y)) (+) (born z) in ((born x) (+) (born y)) (+) (born z) by A43, A45, A49, A48, Lm7;
then A50: x1 * (y + z) == (x1 * y) + (x1 * z) by A2, A3;
set yz1 = y1 + z;
((born x) (+) (born y1)) (+) (born z) in ((born x) (+) (born y)) (+) (born z) by A43, A49, A48, Lm7, A45;
then A51: x * (y1 + z) == (x * y1) + (x * z) by A2, A3;
A52: ((born x1) (+) (born y1)) (+) (born z) in ((born x) (+) (born y)) (+) (born z) by A43, A49, A48, Lm7, A45;
(x1 * z) - (x1 * z) == 0_No by Th39;
then A53: ( (x * z) + ((x1 * z) + (- (x1 * z))) == (x * z) + 0_No & (x * z) + 0_No = x * z ) by Th43;
((x * z) + (x1 * z)) + (- (x1 * z)) == x * z by A53, Th37;
then A54: (((x * z) + (x1 * z)) + (- (x1 * z))) + (- (x1 * y1)) == (x * z) + (- (x1 * y1)) by Th43;
A55: ((x1 * y) + (x * y1)) + ((x * z) + (- (x1 * y1))) = (x1 * y) + ((x * y1) + ((- (x1 * y1)) + (x * z))) by Th37
.= (x1 * y) + (((x * y1) + (- (x1 * y1))) + (x * z)) by Th37
.= ((x1 * y) + ((x * y1) + (- (x1 * y1)))) + (x * z) by Th37
.= (((x1 * y) + (x * y1)) + (- (x1 * y1))) + (x * z) by Th37 ;
A56: - ((x1 * y1) + (x1 * z)) = (- (x1 * y1)) + (- (x1 * z)) by Th40;
y1 + z in Y ++ {z} by A49, A45, Def8;
then A57: ((x1 * (y + z)) + (x * (y1 + z))) - (x1 * (y1 + z)) in comp (X,x,(y + z),(Y ++ {z})) by A45, Def15;
A58: - (x1 * (y1 + z)) == (- (x1 * z)) + (- (x1 * y1)) by A52, A2, A3, Th65, A56;
(x1 * (y + z)) + (x * (y1 + z)) == ((x1 * y) + (x * y1)) + ((x * z) + (x1 * z)) by A47, A50, A51, Th43;
then ((x1 * (y + z)) + (x * (y1 + z))) + (- (x1 * (y1 + z))) == (((x1 * y) + (x * y1)) + ((x * z) + (x1 * z))) + ((- (x1 * z)) + (- (x1 * y1))) by A58, Th43;
then ((x1 * (y + z)) + (x * (y1 + z))) + (- (x1 * (y1 + z))) == ((x1 * y) + (x * y1)) + (((x * z) + (x1 * z)) + ((- (x1 * z)) + (- (x1 * y1)))) by Th37;
then A59: ((x1 * (y + z)) + (x * (y1 + z))) + (- (x1 * (y1 + z))) == ((x1 * y) + (x * y1)) + ((((x * z) + (x1 * z)) + (- (x1 * z))) + (- (x1 * y1))) by Th37;
((x1 * y) + (x * y1)) + ((((x * z) + (x1 * z)) + (- (x1 * z))) + (- (x1 * y1))) == ((x1 * y) + (x * y1)) + ((x * z) + (- (x1 * y1))) by A54, Th43;
hence ex b being Surreal st
( b in comp (X,x,(y + z),(Y ++ {z})) & o == b ) by A57, A44, A46, A55, A45, A59, SURREALO:10; :: thesis: verum

end;

hence (comp (X,x,y,Y)) ++ {(x * z)} <=_ comp (X,x,(y + z),(Y ++ {z})) by Th61; :: according to SURREALO:def 4 :: thesis: comp (X,x,(y + z),(Y ++ {z})) <=_ (comp (X,x,y,Y)) ++ {(x * z)}
for o being Surreal st o in comp (X,x,(y + z),(Y ++ {z})) holds
ex b being Surreal st
( b in (comp (X,x,y,Y)) ++ {(x * z)} & o == b )

proof

let o be Surreal; :: thesis: ( o in comp (X,x,(y + z),(Y ++ {z})) implies ex b being Surreal st
( b in (comp (X,x,y,Y)) ++ {(x * z)} & o == b ) )
assume o in comp (X,x,(y + z),(Y ++ {z})) ; :: thesis: ex b being Surreal st
( b in (comp (X,x,y,Y)) ++ {(x * z)} & o == b )
then consider x1, yz1 being Surreal such that
A60: ( o = ((x1 * (y + z)) + (x * yz1)) - (x1 * yz1) & x1 in X & yz1 in Y ++ {z} ) by Def15;
consider y1, z1 being Surreal such that
A61: ( y1 in Y & z1 in {z} & yz1 = y1 + z1 ) by A60, Def8;
A62: z1 = z by A61, TARSKI:def 1;
A63: ((x1 * y) + (x1 * z)) + ((x * y1) + (x * z)) = (x1 * y) + ((x1 * z) + ((x * z) + (x * y1))) by Th37
.= (x1 * y) + (((x1 * z) + (x * z)) + (x * y1)) by Th37
.= ((x1 * y) + (x * y1)) + ((x1 * z) + (x * z)) by Th37 ;
A64: ( R_ x <> {x} & {x} <> L_ x & R_ y <> {y} & {y} <> L_ y ) by SURREALO:2;
A65: ( x in {x} & y in {y} & z in {z} ) by TARSKI:def 1;
((born x1) (+) (born y)) (+) (born z) in ((born x) (+) (born y)) (+) (born z) by A43, A65, A64, A60, Lm7;
then A66: x1 * (y + z) == (x1 * y) + (x1 * z) by A2, A3;
((born x) (+) (born y1)) (+) (born z1) in ((born x) (+) (born y)) (+) (born z) by A43, A65, A64, Lm7, A61;
then A67: x * yz1 == (x * y1) + (x * z) by A2, A3, A61, A62;
A68: ((born x1) (+) (born y1)) (+) (born z1) in ((born x) (+) (born y)) (+) (born z) by A43, A64, A60, Lm7, A61;
A69: (x1 * z) - (x1 * z) == 0_No by Th39;
A70: ((x1 * y) + (x * y1)) - (x1 * y1) in comp (X,x,y,Y) by A60, A61, Def15;
x * z in {(x * z)} by TARSKI:def 1;
then A71: (((x1 * y) + (x * y1)) + (- (x1 * y1))) + (x * z) in (comp (X,x,y,Y)) ++ {(x * z)} by A70, Def8;
A72: ((x1 * y) + (x * y1)) + ((x * z) + (- (x1 * y1))) = (x1 * y) + ((x * y1) + ((- (x1 * y1)) + (x * z))) by Th37
.= (x1 * y) + (((x * y1) + (- (x1 * y1))) + (x * z)) by Th37
.= ((x1 * y) + ((x * y1) + (- (x1 * y1)))) + (x * z) by Th37
.= (((x1 * y) + (x * y1)) + (- (x1 * y1))) + (x * z) by Th37 ;
A73: - ((x1 * y1) + (x1 * z)) = (- (x1 * y1)) + (- (x1 * z)) by Th40;
A74: - (x1 * yz1) == (- (x1 * z)) + (- (x1 * y1)) by A73, A68, A2, A3, A61, A62, Th65;
A75: (x1 * (y + z)) + (x * yz1) == ((x1 * y) + (x * y1)) + ((x * z) + (x1 * z)) by A66, A67, A63, Th43;
A76: o == (((x1 * y) + (x * y1)) + ((x * z) + (x1 * z))) + ((- (x1 * z)) + (- (x1 * y1))) by A60, Th43, A74, A75;
A77: (((x1 * y) + (x * y1)) + ((x * z) + (x1 * z))) + ((- (x1 * z)) + (- (x1 * y1))) = ((x1 * y) + (x * y1)) + (((x * z) + (x1 * z)) + ((- (x1 * y1)) + (- (x1 * z)))) by Th37
.= ((x1 * y) + (x * y1)) + ((((x * z) + (x1 * z)) + (- (x1 * y1))) + (- (x1 * z))) by Th37
.= ((x1 * y) + (x * y1)) + ((((x * z) + (- (x1 * y1))) + (x1 * z)) + (- (x1 * z))) by Th37
.= ((x1 * y) + (x * y1)) + (((x * z) + (- (x1 * y1))) + ((x1 * z) + (- (x1 * z)))) by Th37
.= ((((x1 * y) + (x * y1)) + (- (x1 * y1))) + (x * z)) + ((x1 * z) + (- (x1 * z))) by A72, Th37 ;
((((x1 * y) + (x * y1)) + (- (x1 * y1))) + (x * z)) + ((x1 * z) + (- (x1 * z))) == ((((x1 * y) + (x * y1)) + (- (x1 * y1))) + (x * z)) + 0_No by A69, Th43;
hence ex b being Surreal st
( b in (comp (X,x,y,Y)) ++ {(x * z)} & o == b ) by A76, SURREALO:10, A71, A77; :: thesis: verum

end;

hence comp (X,x,(y + z),(Y ++ {z})) <=_ (comp (X,x,y,Y)) ++ {(x * z)} by Th61; :: thesis: verum

end;

A78: comp ((L_ x),x,(y + z),((L_ y) ++ {z})) <==> (comp ((L_ x),x,y,(L_ y))) ++ {(x * z)} by A42;
comp ((L_ x),x,(y + z),({y} ++ (L_ z))) <==> (comp ((L_ x),x,z,(L_ z))) ++ {(x * y)} by A13;
then A79: comp ((L_ x),x,(y + z),(L_ (y + z))) <==> ((comp ((L_ x),x,y,(L_ y))) ++ {(x * z)}) \/ ((comp ((L_ x),x,z,(L_ z))) ++ {(x * y)}) by A78, SURREALO:31, A9;
A80: comp ((R_ x),x,(y + z),((R_ y) ++ {z})) <==> (comp ((R_ x),x,y,(R_ y))) ++ {(x * z)} by A42;
comp ((R_ x),x,(y + z),({y} ++ (R_ z))) <==> (comp ((R_ x),x,z,(R_ z))) ++ {(x * y)} by A13;
then A81: comp ((R_ x),x,(y + z),(R_ (y + z))) <==> ((comp ((R_ x),x,y,(R_ y))) ++ {(x * z)}) \/ ((comp ((R_ x),x,z,(R_ z))) ++ {(x * y)}) by A80, SURREALO:31, A11;
(((comp ((L_ x),x,y,(L_ y))) ++ {(x * z)}) \/ ((comp ((L_ x),x,z,(L_ z))) ++ {(x * y)})) \/ (((comp ((R_ x),x,y,(R_ y))) ++ {(x * z)}) \/ ((comp ((R_ x),x,z,(R_ z))) ++ {(x * y)})) = ((((comp ((L_ x),x,y,(L_ y))) ++ {(x * z)}) \/ ((comp ((L_ x),x,z,(L_ z))) ++ {(x * y)})) \/ ((comp ((R_ x),x,z,(R_ z))) ++ {(x * y)})) \/ ((comp ((R_ x),x,y,(R_ y))) ++ {(x * z)}) by XBOOLE_1:4
.= (((comp ((L_ x),x,y,(L_ y))) ++ {(x * z)}) \/ (((comp ((L_ x),x,z,(L_ z))) ++ {(x * y)}) \/ ((comp ((R_ x),x,z,(R_ z))) ++ {(x * y)}))) \/ ((comp ((R_ x),x,y,(R_ y))) ++ {(x * z)}) by XBOOLE_1:4
.= (((comp ((L_ x),x,y,(L_ y))) ++ {(x * z)}) \/ ((comp ((R_ x),x,y,(R_ y))) ++ {(x * z)})) \/ (((comp ((L_ x),x,z,(L_ z))) ++ {(x * y)}) \/ ((comp ((R_ x),x,z,(R_ z))) ++ {(x * y)})) by XBOOLE_1:4
.= (((comp ((L_ x),x,y,(L_ y))) \/ (comp ((R_ x),x,y,(R_ y)))) ++ {(x * z)}) \/ (((comp ((L_ x),x,z,(L_ z))) ++ {(x * y)}) \/ ((comp ((R_ x),x,z,(R_ z))) ++ {(x * y)})) by Th33
.= ((x * y) + (x * z)) `1 by A8, Th33, A5, A4 ;
then A82: L_ (x * (y + z)) <==> L_ ((x * y) + (x * z)) by A81, A7, A79, SURREALO:31;
A83: comp ((L_ x),x,(y + z),((R_ y) ++ {z})) <==> (comp ((L_ x),x,y,(R_ y))) ++ {(x * z)} by A42;
comp ((L_ x),x,(y + z),({y} ++ (R_ z))) <==> (comp ((L_ x),x,z,(R_ z))) ++ {(x * y)} by A13;
then A84: comp ((L_ x),x,(y + z),(R_ (y + z))) <==> ((comp ((L_ x),x,y,(R_ y))) ++ {(x * z)}) \/ ((comp ((L_ x),x,z,(R_ z))) ++ {(x * y)}) by A83, SURREALO:31, A12;
A85: comp ((R_ x),x,(y + z),((L_ y) ++ {z})) <==> (comp ((R_ x),x,y,(L_ y))) ++ {(x * z)} by A42;
comp ((R_ x),x,(y + z),({y} ++ (L_ z))) <==> (comp ((R_ x),x,z,(L_ z))) ++ {(x * y)} by A13;
then A86: comp ((R_ x),x,(y + z),(L_ (y + z))) <==> ((comp ((R_ x),x,y,(L_ y))) ++ {(x * z)}) \/ ((comp ((R_ x),x,z,(L_ z))) ++ {(x * y)}) by A85, SURREALO:31, A10;
A87: R_ (x * (y + z)) <==> (((comp ((L_ x),x,y,(R_ y))) ++ {(x * z)}) \/ ((comp ((L_ x),x,z,(R_ z))) ++ {(x * y)})) \/ (((comp ((R_ x),x,y,(L_ y))) ++ {(x * z)}) \/ ((comp ((R_ x),x,z,(L_ z))) ++ {(x * y)})) by A7, A84, A86, SURREALO:31;
(((comp ((L_ x),x,y,(R_ y))) ++ {(x * z)}) \/ ((comp ((L_ x),x,z,(R_ z))) ++ {(x * y)})) \/ (((comp ((R_ x),x,y,(L_ y))) ++ {(x * z)}) \/ ((comp ((R_ x),x,z,(L_ z))) ++ {(x * y)})) = ((((comp ((L_ x),x,y,(R_ y))) ++ {(x * z)}) \/ ((comp ((L_ x),x,z,(R_ z))) ++ {(x * y)})) \/ ((comp ((R_ x),x,z,(L_ z))) ++ {(x * y)})) \/ ((comp ((R_ x),x,y,(L_ y))) ++ {(x * z)}) by XBOOLE_1:4
.= (((comp ((L_ x),x,y,(R_ y))) ++ {(x * z)}) \/ (((comp ((L_ x),x,z,(R_ z))) ++ {(x * y)}) \/ ((comp ((R_ x),x,z,(L_ z))) ++ {(x * y)}))) \/ ((comp ((R_ x),x,y,(L_ y))) ++ {(x * z)}) by XBOOLE_1:4
.= (((comp ((L_ x),x,y,(R_ y))) ++ {(x * z)}) \/ ((comp ((R_ x),x,y,(L_ y))) ++ {(x * z)})) \/ (((comp ((L_ x),x,z,(R_ z))) ++ {(x * y)}) \/ ((comp ((R_ x),x,z,(L_ z))) ++ {(x * y)})) by XBOOLE_1:4
.= (((comp ((L_ x),x,y,(R_ y))) \/ (comp ((R_ x),x,y,(L_ y)))) ++ {(x * z)}) \/ (((comp ((L_ x),x,z,(R_ z))) ++ {(x * y)}) \/ ((comp ((R_ x),x,z,(L_ z))) ++ {(x * y)})) by Th33
.= ((x * y) + (x * z)) `2 by Th33, A8, A4, A5 ;
hence x * (y + z) == (x * y) + (x * z) by A87, A7, A8, A82, SURREALO:29; :: thesis: verum

end;

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