let x, y be Surreal; :: thesis: 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))))]
set Bx = born x;
set By = born y;
set A = (born x) (+) (born y);
deffunc H1( object , object , Function-yielding c=-monotone Sequence) -> object = [(((((union (rng $3)) .: [:(L_ $1),{$2}:]) ++ ((union (rng $3)) .: [:{$1},(L_ $2):])) ++ (-- ((union (rng $3)) .: [:(L_ $1),(L_ $2):]))) \/ ((((union (rng $3)) .: [:(R_ $1),{$2}:]) ++ ((union (rng $3)) .: [:{$1},(R_ $2):])) ++ (-- ((union (rng $3)) .: [:(R_ $1),(R_ $2):])))),(((((union (rng $3)) .: [:(L_ $1),{$2}:]) ++ ((union (rng $3)) .: [:{$1},(R_ $2):])) ++ (-- ((union (rng $3)) .: [:(L_ $1),(R_ $2):]))) \/ ((((union (rng $3)) .: [:(R_ $1),{$2}:]) ++ ((union (rng $3)) .: [:{$1},(L_ $2):])) ++ (-- ((union (rng $3)) .: [:(R_ ($1 `2)),(L_ $2):]))))];
deffunc H2( object , Function-yielding c=-monotone Sequence) -> object = [( { ((((union (rng $2)) . [xL,(R_ $1)]) +' ((union (rng $2)) . [(L_ $1),yL])) +' (-' ((union (rng $2)) . [xL,yL]))) where xL is Element of L_ (L_ $1), yL is Element of L_ (R_ $1) : ( xL in L_ (L_ $1) & yL in L_ (R_ $1) ) } \/ { ((((union (rng $2)) . [xR,(R_ $1)]) +' ((union (rng $2)) . [(L_ $1),yR])) +' (-' ((union (rng $2)) . [xR,yR]))) where xR is Element of R_ (L_ $1), yR is Element of R_ (R_ $1) : ( xR in R_ (L_ $1) & yR in R_ (R_ $1) ) } ),( { ((((union (rng $2)) . [xL,(R_ $1)]) +' ((union (rng $2)) . [(L_ $1),yR])) +' (-' ((union (rng $2)) . [xL,yR]))) where xL is Element of L_ (L_ $1), yR is Element of R_ (R_ $1) : ( xL in L_ (L_ $1) & yR in R_ (R_ $1) ) } \/ { ((((union (rng $2)) . [xR,(R_ $1)]) +' ((union (rng $2)) . [(L_ $1),yL])) +' (-' ((union (rng $2)) . [xR,yL]))) where xR is Element of R_ (L_ $1), yL is Element of L_ (R_ $1) : ( xR in R_ (L_ $1) & yL in L_ (R_ $1) ) } )];
consider S being Function-yielding c=-monotone Sequence such that
A1: ( dom S = succ ((born x) (+) (born y)) & No_mult_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 = H2(x,S | B) ) ) by Def12;
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 = H2(x,S | ((born x) (+) (born y))) by A2, ORDINAL1:6;
set U = union (rng (S | ((born x) (+) (born y))));
A5: [x,y] in Triangle ((born x) (+) (born y)) by Def5;
A6: x * y = H2([x,y],S | ((born x) (+) (born y))) by A1, A3, A5, A4;
A7: for X, Y being surreal-membered set st X c= (L_ x) \/ (R_ x) & Y c= (L_ y) \/ (R_ y) holds
{ ((((union (rng (S | ((born x) (+) (born y))))) . [xL,y]) +' ((union (rng (S | ((born x) (+) (born y))))) . [x,yL])) +' (-' ((union (rng (S | ((born x) (+) (born y))))) . [xL,yL]))) where xL is Element of X, yL is Element of Y : ( xL in X & yL in Y ) } = comp (X,x,y,Y)
proof
let X, Y be surreal-membered set ; :: thesis: ( X c= (L_ x) \/ (R_ x) & Y c= (L_ y) \/ (R_ y) implies { ((((union (rng (S | ((born x) (+) (born y))))) . [xL,y]) +' ((union (rng (S | ((born x) (+) (born y))))) . [x,yL])) +' (-' ((union (rng (S | ((born x) (+) (born y))))) . [xL,yL]))) where xL is Element of X, yL is Element of Y : ( xL in X & yL in Y ) } = comp (X,x,y,Y) )
assume A8: ( X c= (L_ x) \/ (R_ x) & Y c= (L_ y) \/ (R_ y) ) ; :: thesis: { ((((union (rng (S | ((born x) (+) (born y))))) . [xL,y]) +' ((union (rng (S | ((born x) (+) (born y))))) . [x,yL])) +' (-' ((union (rng (S | ((born x) (+) (born y))))) . [xL,yL]))) where xL is Element of X, yL is Element of Y : ( xL in X & yL in Y ) } = comp (X,x,y,Y)
thus { ((((union (rng (S | ((born x) (+) (born y))))) . [xL,y]) +' ((union (rng (S | ((born x) (+) (born y))))) . [x,yL])) +' (-' ((union (rng (S | ((born x) (+) (born y))))) . [xL,yL]))) where xL is Element of X, yL is Element of Y : ( xL in X & yL in Y ) } c= comp (X,x,y,Y) :: according to XBOOLE_0:def 10 :: thesis: comp (X,x,y,Y) c= { ((((union (rng (S | ((born x) (+) (born y))))) . [xL,y]) +' ((union (rng (S | ((born x) (+) (born y))))) . [x,yL])) +' (-' ((union (rng (S | ((born x) (+) (born y))))) . [xL,yL]))) where xL is Element of X, yL is Element of Y : ( xL in X & yL in Y ) }
proof
let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in { ((((union (rng (S | ((born x) (+) (born y))))) . [xL,y]) +' ((union (rng (S | ((born x) (+) (born y))))) . [x,yL])) +' (-' ((union (rng (S | ((born x) (+) (born y))))) . [xL,yL]))) where xL is Element of X, yL is Element of Y : ( xL in X & yL in Y ) } or a in comp (X,x,y,Y) )
assume a in { ((((union (rng (S | ((born x) (+) (born y))))) . [xL,y]) +' ((union (rng (S | ((born x) (+) (born y))))) . [x,yL])) +' (-' ((union (rng (S | ((born x) (+) (born y))))) . [xL,yL]))) where xL is Element of X, yL is Element of Y : ( xL in X & yL in Y ) } ; :: thesis: a in comp (X,x,y,Y)
then consider xL being Element of X, yL being Element of Y such that
A9: ( a = (((union (rng (S | ((born x) (+) (born y))))) . [xL,y]) +' ((union (rng (S | ((born x) (+) (born y))))) . [x,yL])) +' (-' ((union (rng (S | ((born x) (+) (born y))))) . [xL,yL])) & xL in X & yL in Y ) ;
reconsider x1 = xL, y1 = yL as Surreal by SURREAL0:def 16, A9;
set X1 = born x1;
set C1 = (born x1) (+) (born y);
A10: (born x1) (+) (born y) in (born x) (+) (born y) by A9, A8, SURREALO:1, ORDINAL7:94;
then A11: (born x1) (+) (born y) in succ ((born x) (+) (born y)) by ORDINAL1:8;
then consider SC1 being ManySortedSet of Triangle ((born x1) (+) (born y)) such that
A12: S . ((born x1) (+) (born y)) = SC1 and
for x being object st x in Triangle ((born x1) (+) (born y)) holds
SC1 . x = H2(x,S | ((born x1) (+) (born y))) by A2;
A13: dom SC1 = Triangle ((born x1) (+) (born y)) by PARTFUN1:def 2;
A14: [x1,y] in Triangle ((born x1) (+) (born y)) by Def5;
A15: x1 * y = SC1 . [x1,y] by A11, A1, A2, A12, Th48;
A16: SC1 . [x1,y] = (union (rng S)) . [x1,y] by A11, A13, A14, Th2, A1, A12;
A17: (union (rng (S | ((born x) (+) (born y))))) . [x1,y] = x1 * y by A16, A15, A12, Th5, A10, A14, A13;
set Y1 = born y1;
set C2 = (born x) (+) (born y1);
A18: (born x) (+) (born y1) in (born x) (+) (born y) by A9, A8, SURREALO:1, ORDINAL7:94;
then A19: (born x) (+) (born y1) in succ ((born x) (+) (born y)) by ORDINAL1:8;
then consider SC2 being ManySortedSet of Triangle ((born x) (+) (born y1)) such that
A20: S . ((born x) (+) (born y1)) = SC2 and
for x being object st x in Triangle ((born x) (+) (born y1)) holds
SC2 . x = H2(x,S | ((born x) (+) (born y1))) by A2;
A21: dom SC2 = Triangle ((born x) (+) (born y1)) by PARTFUN1:def 2;
A22: [x,y1] in Triangle ((born x) (+) (born y1)) by Def5;
A23: x * y1 = SC2 . [x,y1] by A19, A1, A2, A20, Th48;
A24: SC2 . [x,y1] = (union (rng S)) . [x,y1] by A19, A21, A22, Th2, A1, A20;
A25: (union (rng (S | ((born x) (+) (born y))))) . [x,y1] = x * y1 by A24, A23, A20, Th5, A18, A22, A21;
set C3 = (born x1) (+) (born y1);
( (born x1) (+) (born y1) in (born x) (+) (born y1) & (born x) (+) (born y1) in (born x) (+) (born y) ) by A9, A8, SURREALO:1, ORDINAL7:94;
then A26: (born x1) (+) (born y1) in (born x) (+) (born y) by ORDINAL1:10;
then A27: (born x1) (+) (born y1) in succ ((born x) (+) (born y)) by ORDINAL1:8;
then consider SC3 being ManySortedSet of Triangle ((born x1) (+) (born y1)) such that
A28: S . ((born x1) (+) (born y1)) = SC3 and
for x being object st x in Triangle ((born x1) (+) (born y1)) holds
SC3 . x = H2(x,S | ((born x1) (+) (born y1))) by A2;
A29: dom SC3 = Triangle ((born x1) (+) (born y1)) by PARTFUN1:def 2;
A30: [x1,y1] in Triangle ((born x1) (+) (born y1)) by Def5;
A31: x1 * y1 = SC3 . [x1,y1] by A27, A1, A2, A28, Th48;
A32: SC3 . [x1,y1] = (union (rng S)) . [x1,y1] by A27, A29, A30, Th2, A1, A28;
a = (((union (rng (S | ((born x) (+) (born y))))) . [xL,y]) +' ((union (rng (S | ((born x) (+) (born y))))) . [x,yL])) +' (-' (x1 * y1)) by A9, A32, A31, A28, Th5, A26, A30, A29;
hence a in comp (X,x,y,Y) by Def14, A9, A17, A25; :: thesis: verum
end;
let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in comp (X,x,y,Y) or a in { ((((union (rng (S | ((born x) (+) (born y))))) . [xL,y]) +' ((union (rng (S | ((born x) (+) (born y))))) . [x,yL])) +' (-' ((union (rng (S | ((born x) (+) (born y))))) . [xL,yL]))) where xL is Element of X, yL is Element of Y : ( xL in X & yL in Y ) } )
assume a in comp (X,x,y,Y) ; :: thesis: a in { ((((union (rng (S | ((born x) (+) (born y))))) . [xL,y]) +' ((union (rng (S | ((born x) (+) (born y))))) . [x,yL])) +' (-' ((union (rng (S | ((born x) (+) (born y))))) . [xL,yL]))) where xL is Element of X, yL is Element of Y : ( xL in X & yL in Y ) }
then consider x1, y1 being Surreal such that
A33: ( a = ((x1 * y) +' (x * y1)) +' (-' (x1 * y1)) & x1 in X & y1 in Y ) by Def14;
set X1 = born x1;
set C1 = (born x1) (+) (born y);
A34: (born x1) (+) (born y) in (born x) (+) (born y) by A33, A8, SURREALO:1, ORDINAL7:94;
then A35: (born x1) (+) (born y) in succ ((born x) (+) (born y)) by ORDINAL1:8;
then consider SC1 being ManySortedSet of Triangle ((born x1) (+) (born y)) such that
A36: S . ((born x1) (+) (born y)) = SC1 and
for x being object st x in Triangle ((born x1) (+) (born y)) holds
SC1 . x = H2(x,S | ((born x1) (+) (born y))) by A2;
A37: dom SC1 = Triangle ((born x1) (+) (born y)) by PARTFUN1:def 2;
A38: [x1,y] in Triangle ((born x1) (+) (born y)) by Def5;
A39: x1 * y = SC1 . [x1,y] by A35, A1, A2, A36, Th48;
A40: SC1 . [x1,y] = (union (rng S)) . [x1,y] by A35, A37, A38, Th2, A1, A36;
A41: (union (rng (S | ((born x) (+) (born y))))) . [x1,y] = x1 * y by A40, A39, A36, Th5, A34, A38, A37;
set Y1 = born y1;
set C2 = (born x) (+) (born y1);
A42: (born x) (+) (born y1) in (born x) (+) (born y) by A33, A8, SURREALO:1, ORDINAL7:94;
then A43: (born x) (+) (born y1) in succ ((born x) (+) (born y)) by ORDINAL1:8;
then consider SC2 being ManySortedSet of Triangle ((born x) (+) (born y1)) such that
A44: S . ((born x) (+) (born y1)) = SC2 and
for x being object st x in Triangle ((born x) (+) (born y1)) holds
SC2 . x = H2(x,S | ((born x) (+) (born y1))) by A2;
A45: dom SC2 = Triangle ((born x) (+) (born y1)) by PARTFUN1:def 2;
A46: [x,y1] in Triangle ((born x) (+) (born y1)) by Def5;
A47: x * y1 = SC2 . [x,y1] by A43, A1, A2, A44, Th48;
A48: SC2 . [x,y1] = (union (rng S)) . [x,y1] by A43, A45, A46, Th2, A1, A44;
A49: (union (rng (S | ((born x) (+) (born y))))) . [x,y1] = x * y1 by A48, A47, A44, Th5, A42, A46, A45;
set C3 = (born x1) (+) (born y1);
( (born x1) (+) (born y1) in (born x) (+) (born y1) & (born x) (+) (born y1) in (born x) (+) (born y) ) by A33, A8, SURREALO:1, ORDINAL7:94;
then A50: (born x1) (+) (born y1) in (born x) (+) (born y) by ORDINAL1:10;
then A51: (born x1) (+) (born y1) in succ ((born x) (+) (born y)) by ORDINAL1:8;
then consider SC3 being ManySortedSet of Triangle ((born x1) (+) (born y1)) such that
A52: S . ((born x1) (+) (born y1)) = SC3 and
for x being object st x in Triangle ((born x1) (+) (born y1)) holds
SC3 . x = H2(x,S | ((born x1) (+) (born y1))) by A2;
A53: dom SC3 = Triangle ((born x1) (+) (born y1)) by PARTFUN1:def 2;
A54: [x1,y1] in Triangle ((born x1) (+) (born y1)) by Def5;
A55: x1 * y1 = SC3 . [x1,y1] by A51, A1, A2, A52, Th48;
A56: SC3 . [x1,y1] = (union (rng S)) . [x1,y1] by A51, A53, A54, Th2, A1, A52;
a = ((x1 * y) +' (x * y1)) +' (-' ((union (rng (S | ((born x) (+) (born y))))) . [x1,y1])) by A33, A56, A55, A52, Th5, A50, A54, A53;
hence a in { ((((union (rng (S | ((born x) (+) (born y))))) . [xL,y]) +' ((union (rng (S | ((born x) (+) (born y))))) . [x,yL])) +' (-' ((union (rng (S | ((born x) (+) (born y))))) . [xL,yL]))) where xL is Element of X, yL is Element of Y : ( xL in X & yL in Y ) } by A33, A49, A41; :: thesis: verum
end;
A57: ( L_ x c= (L_ x) \/ (R_ x) & R_ x c= (L_ x) \/ (R_ x) & L_ y c= (L_ y) \/ (R_ y) & R_ y c= (L_ y) \/ (R_ y) ) by XBOOLE_1:7;
A58: { ((((union (rng (S | ((born x) (+) (born y))))) . [xL,y]) +' ((union (rng (S | ((born x) (+) (born y))))) . [x,yL])) +' (-' ((union (rng (S | ((born x) (+) (born y))))) . [xL,yL]))) where xL is Element of L_ x, yL is Element of L_ y : ( xL in L_ x & yL in L_ y ) } = comp ((L_ x),x,y,(L_ y)) by A57, A7;
A59: { ((((union (rng (S | ((born x) (+) (born y))))) . [xL,y]) +' ((union (rng (S | ((born x) (+) (born y))))) . [x,yR])) +' (-' ((union (rng (S | ((born x) (+) (born y))))) . [xL,yR]))) where xL is Element of L_ x, yR is Element of R_ y : ( xL in L_ x & yR in R_ y ) } = comp ((L_ x),x,y,(R_ y)) by A57, A7;
{ ((((union (rng (S | ((born x) (+) (born y))))) . [xR,y]) +' ((union (rng (S | ((born x) (+) (born y))))) . [x,yR])) +' (-' ((union (rng (S | ((born x) (+) (born y))))) . [xR,yR]))) where xR is Element of R_ x, yR is Element of R_ y : ( xR in R_ x & yR in R_ y ) } = comp ((R_ x),x,y,(R_ y)) by A57, A7;
hence 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 A6, A58, A59, A57, A7; :: thesis: verum