let r, s be Sequence of REAL ; :: thesis: for y, z being strictly_decreasing Surreal-Sequence
for S, T being non empty Ordinal
for yz being strictly_decreasing uSurreal-Sequence st dom y c= S & dom z c= T & Unique_No ((rng y) ++ (rng z)) c= rng yz & dom y = dom r & dom z = dom s holds
(Sum (r,(No_omega^ y))) * (Sum (s,(No_omega^ z))) == Sum ((Sum (y,z,yz,r,s,S,T)),(No_omega^ yz))
let y, z be strictly_decreasing Surreal-Sequence; :: thesis: for S, T being non empty Ordinal
for yz being strictly_decreasing uSurreal-Sequence st dom y c= S & dom z c= T & Unique_No ((rng y) ++ (rng z)) c= rng yz & dom y = dom r & dom z = dom s holds
(Sum (r,(No_omega^ y))) * (Sum (s,(No_omega^ z))) == Sum ((Sum (y,z,yz,r,s,S,T)),(No_omega^ yz))
let S, T be non empty Ordinal; :: thesis: for yz being strictly_decreasing uSurreal-Sequence st dom y c= S & dom z c= T & Unique_No ((rng y) ++ (rng z)) c= rng yz & dom y = dom r & dom z = dom s holds
(Sum (r,(No_omega^ y))) * (Sum (s,(No_omega^ z))) == Sum ((Sum (y,z,yz,r,s,S,T)),(No_omega^ yz))
let yz be strictly_decreasing uSurreal-Sequence; :: thesis: ( dom y c= S & dom z c= T & Unique_No ((rng y) ++ (rng z)) c= rng yz & dom y = dom r & dom z = dom s implies (Sum (r,(No_omega^ y))) * (Sum (s,(No_omega^ z))) == Sum ((Sum (y,z,yz,r,s,S,T)),(No_omega^ yz)) )
assume that
A1: ( dom y c= S & dom z c= T & Unique_No ((rng y) ++ (rng z)) c= rng yz ) and
A2: ( dom y = dom r & dom z = dom s ) ; :: thesis: (Sum (r,(No_omega^ y))) * (Sum (s,(No_omega^ z))) == Sum ((Sum (y,z,yz,r,s,S,T)),(No_omega^ yz))
set Ny = No_omega^ y;
set Nz = No_omega^ z;
set Nyz = No_omega^ yz;
defpred S1[ Ordinal] means for Y, Z being Ordinal st Y c= dom y & Z c= dom z & Y (+) Z = $1 holds
(Sum ((r | Y),((No_omega^ y) | Y))) * (Sum ((s | Z),((No_omega^ z) | Z))) == Sum ((Sum ((y | Y),(z | Z),yz,(r | Y),(s | Z),S,T)),(No_omega^ yz));
A3: for O being Ordinal st ( for C being Ordinal st C in O holds
S1[C] ) holds
S1[O]
proof
let O be Ordinal; :: thesis: ( ( for C being Ordinal st C in O holds
S1[C] ) implies S1[O] )
assume A4: for C being Ordinal st C in O holds
S1[C] ; :: thesis: S1[O]
let Y, Z be Ordinal; :: thesis: ( Y c= dom y & Z c= dom z & Y (+) Z = O implies (Sum ((r | Y),((No_omega^ y) | Y))) * (Sum ((s | Z),((No_omega^ z) | Z))) == Sum ((Sum ((y | Y),(z | Z),yz,(r | Y),(s | Z),S,T)),(No_omega^ yz)) )
assume A5: ( Y c= dom y & Z c= dom z & Y (+) Z = O ) ; :: thesis: (Sum ((r | Y),((No_omega^ y) | Y))) * (Sum ((s | Z),((No_omega^ z) | Z))) == Sum ((Sum ((y | Y),(z | Z),yz,(r | Y),(s | Z),S,T)),(No_omega^ yz))
reconsider rY = r | Y, sZ = s | Z as Sequence of REAL ;
set yY = y | Y;
set zZ = z | Z;
set P = Sum ((y | Y),(z | Z),yz,rY,sZ,S,T);
set NyY = (No_omega^ y) | Y;
set NzZ = (No_omega^ z) | Z;
A6: ( dom (y | Y) = Y & Y = dom rY & dom (z | Z) = Z & Z = dom sZ ) by A5, A2, RELAT_1:62;
per cases ( ( Y is limit_ordinal & Z is limit_ordinal ) or not Y is limit_ordinal or not Z is limit_ordinal ) ;
suppose A7: ( Y is limit_ordinal & Z is limit_ordinal ) ; :: thesis: (Sum ((r | Y),((No_omega^ y) | Y))) * (Sum ((s | Z),((No_omega^ z) | Z))) == Sum ((Sum ((y | Y),(z | Z),yz,(r | Y),(s | Z),S,T)),(No_omega^ yz))
set Uyz = ord (Unique_No ((rng (y | Y)) ++ (rng (z | Z))));
Unique_No ((rng (y | Y)) ++ (rng (z | Z))) is desc_ordering by Th47;
then A8: rng (ord (Unique_No ((rng (y | Y)) ++ (rng (z | Z))))) = Unique_No ((rng (y | Y)) ++ (rng (z | Z))) by Def13;
then reconsider Uyz = ord (Unique_No ((rng (y | Y)) ++ (rng (z | Z)))) as strictly_decreasing uSurreal-Sequence by SURREALC:def 10;
set NUyz = No_omega^ Uyz;
set PU = Sum ((y | Y),(z | Z),Uyz,rY,sZ,S,T);
( dom (No_omega^ y) = dom y & dom (No_omega^ z) = dom z ) by SURREALC:def 22;
then A9: ( Y c= (dom r) /\ (dom (No_omega^ y)) & Z c= (dom s) /\ (dom (No_omega^ z)) ) by A5, A2;
reconsider SuY = [ { ((Sum ((r | B),((No_omega^ y) | B))) + ((uReal . ((r . B) - e)) * ((No_omega^ y) .. B))) where B is Element of Y, e is positive Real : B in Y } , { ((Sum ((r | B),((No_omega^ y) | B))) + ((uReal . ((r . B) + e)) * ((No_omega^ y) .. B))) where B is Element of Y, e is positive Real : B in Y } ] as Surreal by A9, Th61;
Unique_No SuY = Sum ((r | Y),((No_omega^ y) | Y)) by A9, Th62;
then A10: SuY == Sum ((r | Y),((No_omega^ y) | Y)) by SURREALO:def 10;
reconsider SuZ = [ { ((Sum ((s | B),((No_omega^ z) | B))) + ((uReal . ((s . B) - e)) * ((No_omega^ z) .. B))) where B is Element of Z, e is positive Real : B in Z } , { ((Sum ((s | B),((No_omega^ z) | B))) + ((uReal . ((s . B) + e)) * ((No_omega^ z) .. B))) where B is Element of Z, e is positive Real : B in Z } ] as Surreal by A9, Th61;
Unique_No SuZ = Sum ((s | Z),((No_omega^ z) | Z)) by A9, Th62;
then A11: SuZ == Sum ((s | Z),((No_omega^ z) | Z)) by SURREALO:def 10;
(rng (y | Y)) ++ (rng (z | Z)) c= (rng y) ++ (rng z) by Th34;
then Unique_No ((rng (y | Y)) ++ (rng (z | Z))) c= Unique_No ((rng y) ++ (rng z)) by Th48;
then A12: Unique_No ((rng (y | Y)) ++ (rng (z | Z))) c= rng yz by A1;
( dom (y | Y) c= S & dom (z | Z) c= T ) by A5, A1, A6;
then A13: Sum ((Sum ((y | Y),(z | Z),yz,rY,sZ,S,T)),(No_omega^ yz)) = Sum ((Sum ((y | Y),(z | Z),Uyz,rY,sZ,S,T)),(No_omega^ Uyz)) by A12, Th109, A8;
A14: for Y1, Z1 being Ordinal st Y1 in Y & Z1 in Z holds
for ey, ez being Real
for y1, z1 being Surreal st y1 == (Sum ((r | (succ Y1)),((No_omega^ y) | (succ Y1)))) + ((uReal . ey) * (No_omega^ (y .. Y1))) & z1 == (Sum ((s | (succ Z1)),((No_omega^ z) | (succ Z1)))) + ((uReal . ez) * (No_omega^ (z .. Z1))) holds
for O1 being Ordinal st O1 in dom Uyz & Uyz .. O1 == (y .. Y1) + (z .. Z1) holds
ex T being Surreal st
( |.T.| infinitely< No_omega^ ((y .. Y1) + (z .. Z1)) & ((SuY * z1) + (y1 * SuZ)) - (z1 * y1) == ((Sum (((Sum ((y | Y),(z | Z),Uyz,rY,sZ,S,T)) | (succ O1)),((No_omega^ Uyz) | (succ O1)))) + T) - ((uReal . (ey * ez)) * (No_omega^ ((y .. Y1) + (z .. Z1)))) )
proof
let Y1, Z1 be Ordinal; :: thesis: ( Y1 in Y & Z1 in Z implies for ey, ez being Real
for y1, z1 being Surreal st y1 == (Sum ((r | (succ Y1)),((No_omega^ y) | (succ Y1)))) + ((uReal . ey) * (No_omega^ (y .. Y1))) & z1 == (Sum ((s | (succ Z1)),((No_omega^ z) | (succ Z1)))) + ((uReal . ez) * (No_omega^ (z .. Z1))) holds
for O1 being Ordinal st O1 in dom Uyz & Uyz .. O1 == (y .. Y1) + (z .. Z1) holds
ex T being Surreal st
( |.T.| infinitely< No_omega^ ((y .. Y1) + (z .. Z1)) & ((SuY * z1) + (y1 * SuZ)) - (z1 * y1) == ((Sum (((Sum ((y | Y),(z | Z),Uyz,rY,sZ,S,T)) | (succ O1)),((No_omega^ Uyz) | (succ O1)))) + T) - ((uReal . (ey * ez)) * (No_omega^ ((y .. Y1) + (z .. Z1)))) ) )
assume A15: ( Y1 in Y & Z1 in Z ) ; :: thesis: for ey, ez being Real
for y1, z1 being Surreal st y1 == (Sum ((r | (succ Y1)),((No_omega^ y) | (succ Y1)))) + ((uReal . ey) * (No_omega^ (y .. Y1))) & z1 == (Sum ((s | (succ Z1)),((No_omega^ z) | (succ Z1)))) + ((uReal . ez) * (No_omega^ (z .. Z1))) holds
for O1 being Ordinal st O1 in dom Uyz & Uyz .. O1 == (y .. Y1) + (z .. Z1) holds
ex T being Surreal st
( |.T.| infinitely< No_omega^ ((y .. Y1) + (z .. Z1)) & ((SuY * z1) + (y1 * SuZ)) - (z1 * y1) == ((Sum (((Sum ((y | Y),(z | Z),Uyz,rY,sZ,S,T)) | (succ O1)),((No_omega^ Uyz) | (succ O1)))) + T) - ((uReal . (ey * ez)) * (No_omega^ ((y .. Y1) + (z .. Z1)))) )
set suY = succ Y1;
set suZ = succ Z1;
set NY = No_omega^ (y .. Y1);
set NZ = No_omega^ (z .. Z1);
let ey, ez be Real; :: thesis: for y1, z1 being Surreal st y1 == (Sum ((r | (succ Y1)),((No_omega^ y) | (succ Y1)))) + ((uReal . ey) * (No_omega^ (y .. Y1))) & z1 == (Sum ((s | (succ Z1)),((No_omega^ z) | (succ Z1)))) + ((uReal . ez) * (No_omega^ (z .. Z1))) holds
for O1 being Ordinal st O1 in dom Uyz & Uyz .. O1 == (y .. Y1) + (z .. Z1) holds
ex T being Surreal st
( |.T.| infinitely< No_omega^ ((y .. Y1) + (z .. Z1)) & ((SuY * z1) + (y1 * SuZ)) - (z1 * y1) == ((Sum (((Sum ((y | Y),(z | Z),Uyz,rY,sZ,S,T)) | (succ O1)),((No_omega^ Uyz) | (succ O1)))) + T) - ((uReal . (ey * ez)) * (No_omega^ ((y .. Y1) + (z .. Z1)))) )
set Ry = uReal . ey;
set Rz = uReal . ez;
set Sy = Sum ((r | (succ Y1)),((No_omega^ y) | (succ Y1)));
set Sz = Sum ((s | (succ Z1)),((No_omega^ z) | (succ Z1)));
let y1, z1 be Surreal; :: thesis: ( y1 == (Sum ((r | (succ Y1)),((No_omega^ y) | (succ Y1)))) + ((uReal . ey) * (No_omega^ (y .. Y1))) & z1 == (Sum ((s | (succ Z1)),((No_omega^ z) | (succ Z1)))) + ((uReal . ez) * (No_omega^ (z .. Z1))) implies for O1 being Ordinal st O1 in dom Uyz & Uyz .. O1 == (y .. Y1) + (z .. Z1) holds
ex T being Surreal st
( |.T.| infinitely< No_omega^ ((y .. Y1) + (z .. Z1)) & ((SuY * z1) + (y1 * SuZ)) - (z1 * y1) == ((Sum (((Sum ((y | Y),(z | Z),Uyz,rY,sZ,S,T)) | (succ O1)),((No_omega^ Uyz) | (succ O1)))) + T) - ((uReal . (ey * ez)) * (No_omega^ ((y .. Y1) + (z .. Z1)))) ) )
assume A16: ( y1 == (Sum ((r | (succ Y1)),((No_omega^ y) | (succ Y1)))) + ((uReal . ey) * (No_omega^ (y .. Y1))) & z1 == (Sum ((s | (succ Z1)),((No_omega^ z) | (succ Z1)))) + ((uReal . ez) * (No_omega^ (z .. Z1))) ) ; :: thesis: for O1 being Ordinal st O1 in dom Uyz & Uyz .. O1 == (y .. Y1) + (z .. Z1) holds
ex T being Surreal st
( |.T.| infinitely< No_omega^ ((y .. Y1) + (z .. Z1)) & ((SuY * z1) + (y1 * SuZ)) - (z1 * y1) == ((Sum (((Sum ((y | Y),(z | Z),Uyz,rY,sZ,S,T)) | (succ O1)),((No_omega^ Uyz) | (succ O1)))) + T) - ((uReal . (ey * ez)) * (No_omega^ ((y .. Y1) + (z .. Z1)))) )
let O1 be Ordinal; :: thesis: ( O1 in dom Uyz & Uyz .. O1 == (y .. Y1) + (z .. Z1) implies ex T being Surreal st
( |.T.| infinitely< No_omega^ ((y .. Y1) + (z .. Z1)) & ((SuY * z1) + (y1 * SuZ)) - (z1 * y1) == ((Sum (((Sum ((y | Y),(z | Z),Uyz,rY,sZ,S,T)) | (succ O1)),((No_omega^ Uyz) | (succ O1)))) + T) - ((uReal . (ey * ez)) * (No_omega^ ((y .. Y1) + (z .. Z1)))) ) )
assume A17: ( O1 in dom Uyz & Uyz .. O1 == (y .. Y1) + (z .. Z1) ) ; :: thesis: ex T being Surreal st
( |.T.| infinitely< No_omega^ ((y .. Y1) + (z .. Z1)) & ((SuY * z1) + (y1 * SuZ)) - (z1 * y1) == ((Sum (((Sum ((y | Y),(z | Z),Uyz,rY,sZ,S,T)) | (succ O1)),((No_omega^ Uyz) | (succ O1)))) + T) - ((uReal . (ey * ez)) * (No_omega^ ((y .. Y1) + (z .. Z1)))) )
set OPC = ((SuY * z1) + (y1 * SuZ)) - (z1 * y1);
( SuY * z1 == SuY * ((Sum ((s | (succ Z1)),((No_omega^ z) | (succ Z1)))) + ((uReal . ez) * (No_omega^ (z .. Z1)))) & y1 * SuZ == ((Sum ((r | (succ Y1)),((No_omega^ y) | (succ Y1)))) + ((uReal . ey) * (No_omega^ (y .. Y1)))) * SuZ ) by A16, SURREALR:54;
then ( (SuY * z1) + (y1 * SuZ) == (SuY * ((Sum ((s | (succ Z1)),((No_omega^ z) | (succ Z1)))) + ((uReal . ez) * (No_omega^ (z .. Z1))))) + (((Sum ((r | (succ Y1)),((No_omega^ y) | (succ Y1)))) + ((uReal . ey) * (No_omega^ (y .. Y1)))) * SuZ) & z1 * y1 == ((Sum ((r | (succ Y1)),((No_omega^ y) | (succ Y1)))) + ((uReal . ey) * (No_omega^ (y .. Y1)))) * ((Sum ((s | (succ Z1)),((No_omega^ z) | (succ Z1)))) + ((uReal . ez) * (No_omega^ (z .. Z1)))) ) by A16, SURREALR:66, Th29;
then A18: ((SuY * z1) + (y1 * SuZ)) - (z1 * y1) == ((SuY * ((Sum ((s | (succ Z1)),((No_omega^ z) | (succ Z1)))) + ((uReal . ez) * (No_omega^ (z .. Z1))))) + (((Sum ((r | (succ Y1)),((No_omega^ y) | (succ Y1)))) + ((uReal . ey) * (No_omega^ (y .. Y1)))) * SuZ)) - (((Sum ((r | (succ Y1)),((No_omega^ y) | (succ Y1)))) + ((uReal . ey) * (No_omega^ (y .. Y1)))) * ((Sum ((s | (succ Z1)),((No_omega^ z) | (succ Z1)))) + ((uReal . ez) * (No_omega^ (z .. Z1))))) by Th28;
((SuY * ((Sum ((s | (succ Z1)),((No_omega^ z) | (succ Z1)))) + ((uReal . ez) * (No_omega^ (z .. Z1))))) + (((Sum ((r | (succ Y1)),((No_omega^ y) | (succ Y1)))) + ((uReal . ey) * (No_omega^ (y .. Y1)))) * SuZ)) - (((Sum ((r | (succ Y1)),((No_omega^ y) | (succ Y1)))) + ((uReal . ey) * (No_omega^ (y .. Y1)))) * ((Sum ((s | (succ Z1)),((No_omega^ z) | (succ Z1)))) + ((uReal . ez) * (No_omega^ (z .. Z1))))) == ((((SuY * (Sum ((s | (succ Z1)),((No_omega^ z) | (succ Z1))))) + ((Sum ((r | (succ Y1)),((No_omega^ y) | (succ Y1)))) * SuZ)) - ((Sum ((r | (succ Y1)),((No_omega^ y) | (succ Y1)))) * (Sum ((s | (succ Z1)),((No_omega^ z) | (succ Z1)))))) + (((SuY - (Sum ((r | (succ Y1)),((No_omega^ y) | (succ Y1))))) * ((uReal . ez) * (No_omega^ (z .. Z1)))) + ((SuZ - (Sum ((s | (succ Z1)),((No_omega^ z) | (succ Z1))))) * ((uReal . ey) * (No_omega^ (y .. Y1)))))) - (((uReal . ez) * (No_omega^ (z .. Z1))) * ((uReal . ey) * (No_omega^ (y .. Y1)))) by Th103;
then A19: ((SuY * z1) + (y1 * SuZ)) - (z1 * y1) == ((((SuY * (Sum ((s | (succ Z1)),((No_omega^ z) | (succ Z1))))) + ((Sum ((r | (succ Y1)),((No_omega^ y) | (succ Y1)))) * SuZ)) - ((Sum ((r | (succ Y1)),((No_omega^ y) | (succ Y1)))) * (Sum ((s | (succ Z1)),((No_omega^ z) | (succ Z1)))))) + (((SuY - (Sum ((r | (succ Y1)),((No_omega^ y) | (succ Y1))))) * ((uReal . ez) * (No_omega^ (z .. Z1)))) + ((SuZ - (Sum ((s | (succ Z1)),((No_omega^ z) | (succ Z1))))) * ((uReal . ey) * (No_omega^ (y .. Y1)))))) - (((uReal . ez) * (No_omega^ (z .. Z1))) * ((uReal . ey) * (No_omega^ (y .. Y1)))) by A18, SURREALO:4;
A20: succ Y1 in Y by A7, A15, ORDINAL1:28;
A21: succ Y1 c= Y by A7, A15, ORDINAL1:28, ORDINAL1:def 2;
then A22: succ Y1 c= dom y by A5;
A23: succ Z1 in Z by A7, A15, ORDINAL1:28;
A24: succ Z1 c= Z by ORDINAL1:def 2, A7, A15, ORDINAL1:28;
then A25: succ Z1 c= dom z by A5;
A26: ( y | (succ Y1) = (y | Y) | (succ Y1) & r | (succ Y1) = rY | (succ Y1) & z | (succ Z1) = (z | Z) | (succ Z1) & s | (succ Z1) = sZ | (succ Z1) ) by A21, A24, RELAT_1:74;
A27: ( No_omega^ (y | Y) = (No_omega^ y) | Y & No_omega^ (y | (succ Y1)) = (No_omega^ y) | (succ Y1) ) by SURREALC:88;
A28: ( No_omega^ (z | Z) = (No_omega^ z) | Z & No_omega^ (z | (succ Z1)) = (No_omega^ z) | (succ Z1) ) by SURREALC:88;
set Pyz = Sum (((y | Y) /^ (succ Y1)),((z | Z) /^ (succ Z1)),yz,(rY /^ (succ Y1)),(sZ /^ (succ Z1)),S,T);
A29: ((SuY * (Sum ((s | (succ Z1)),((No_omega^ z) | (succ Z1))))) + ((Sum ((r | (succ Y1)),((No_omega^ y) | (succ Y1)))) * SuZ)) - ((Sum ((r | (succ Y1)),((No_omega^ y) | (succ Y1)))) * (Sum ((s | (succ Z1)),((No_omega^ z) | (succ Z1))))) == (Sum ((Sum ((y | Y),(z | Z),yz,rY,sZ,S,T)),(No_omega^ yz))) - (Sum ((Sum (((y | Y) /^ (succ Y1)),((z | Z) /^ (succ Z1)),yz,(rY /^ (succ Y1)),(sZ /^ (succ Z1)),S,T)),(No_omega^ yz)))
proof
(succ Y1) (+) Z in Y (+) Z by A20, ORDINAL7:94;
then ( (Sum ((r | (succ Y1)),((No_omega^ y) | (succ Y1)))) * SuZ == (Sum ((r | (succ Y1)),((No_omega^ y) | (succ Y1)))) * (Sum ((s | Z),((No_omega^ z) | Z))) & (Sum ((r | (succ Y1)),((No_omega^ y) | (succ Y1)))) * (Sum ((s | Z),((No_omega^ z) | Z))) == Sum ((Sum ((y | (succ Y1)),(z | Z),yz,(r | (succ Y1)),sZ,S,T)),(No_omega^ yz)) ) by A4, A5, A22, A11, Th29;
then A30: (Sum ((r | (succ Y1)),((No_omega^ y) | (succ Y1)))) * SuZ == Sum ((Sum ((y | (succ Y1)),(z | Z),yz,(r | (succ Y1)),sZ,S,T)),(No_omega^ yz)) by SURREALO:4;
A31: Y (+) (succ Z1) in O by A23, A5, ORDINAL7:94;
then ( SuY * (Sum ((s | (succ Z1)),((No_omega^ z) | (succ Z1)))) == (Sum ((r | Y),((No_omega^ y) | Y))) * (Sum ((s | (succ Z1)),((No_omega^ z) | (succ Z1)))) & (Sum ((r | Y),((No_omega^ y) | Y))) * (Sum ((s | (succ Z1)),((No_omega^ z) | (succ Z1)))) == Sum ((Sum ((y | Y),(z | (succ Z1)),yz,rY,(s | (succ Z1)),S,T)),(No_omega^ yz)) ) by A4, A5, A25, A10, Th29;
then A32: SuY * (Sum ((s | (succ Z1)),((No_omega^ z) | (succ Z1)))) == Sum ((Sum ((y | Y),(z | (succ Z1)),yz,rY,(s | (succ Z1)),S,T)),(No_omega^ yz)) by SURREALO:4;
(succ Y1) (+) (succ Z1) in Y (+) (succ Z1) by A20, ORDINAL7:94;
then A33: (Sum ((r | (succ Y1)),((No_omega^ y) | (succ Y1)))) * (Sum ((s | (succ Z1)),((No_omega^ z) | (succ Z1)))) == Sum ((Sum ((y | (succ Y1)),(z | (succ Z1)),yz,(r | (succ Y1)),(s | (succ Z1)),S,T)),(No_omega^ yz)) by A4, A22, A25, A31, ORDINAL1:10;
(SuY * (Sum ((s | (succ Z1)),((No_omega^ z) | (succ Z1))))) + ((Sum ((r | (succ Y1)),((No_omega^ y) | (succ Y1)))) * SuZ) == (Sum ((Sum ((y | (succ Y1)),(z | Z),yz,(r | (succ Y1)),sZ,S,T)),(No_omega^ yz))) + (Sum ((Sum ((y | Y),(z | (succ Z1)),yz,rY,(s | (succ Z1)),S,T)),(No_omega^ yz))) by A30, A32, SURREALR:66;
then A34: ((SuY * (Sum ((s | (succ Z1)),((No_omega^ z) | (succ Z1))))) + ((Sum ((r | (succ Y1)),((No_omega^ y) | (succ Y1)))) * SuZ)) - ((Sum ((r | (succ Y1)),((No_omega^ y) | (succ Y1)))) * (Sum ((s | (succ Z1)),((No_omega^ z) | (succ Z1))))) == ((Sum ((Sum (((y | Y) | (succ Y1)),(z | Z),yz,(rY | (succ Y1)),sZ,S,T)),(No_omega^ yz))) + (Sum ((Sum ((y | Y),((z | Z) | (succ Z1)),yz,rY,(sZ | (succ Z1)),S,T)),(No_omega^ yz)))) - (Sum ((Sum (((y | Y) | (succ Y1)),((z | Z) | (succ Z1)),yz,(rY | (succ Y1)),(sZ | (succ Z1)),S,T)),(No_omega^ yz))) by A26, A33, Th28;
A35: ( dom (y | Y) c= S & dom (z | Z) c= T ) by A6, A5, A1;
((Sum ((Sum (((y | Y) | (succ Y1)),(z | Z),yz,(rY | (succ Y1)),sZ,S,T)),(No_omega^ yz))) + (Sum ((Sum ((y | Y),((z | Z) | (succ Z1)),yz,rY,(sZ | (succ Z1)),S,T)),(No_omega^ yz)))) - (Sum ((Sum (((y | Y) | (succ Y1)),((z | Z) | (succ Z1)),yz,(rY | (succ Y1)),(sZ | (succ Z1)),S,T)),(No_omega^ yz))) == (Sum ((Sum ((y | Y),(z | Z),yz,rY,sZ,S,T)),(No_omega^ yz))) - (Sum ((Sum (((y | Y) /^ (succ Y1)),((z | Z) /^ (succ Z1)),yz,(rY /^ (succ Y1)),(sZ /^ (succ Z1)),S,T)),(No_omega^ yz))) by A35, A21, A24, A6, Th107;
hence ((SuY * (Sum ((s | (succ Z1)),((No_omega^ z) | (succ Z1))))) + ((Sum ((r | (succ Y1)),((No_omega^ y) | (succ Y1)))) * SuZ)) - ((Sum ((r | (succ Y1)),((No_omega^ y) | (succ Y1)))) * (Sum ((s | (succ Z1)),((No_omega^ z) | (succ Z1))))) == (Sum ((Sum ((y | Y),(z | Z),yz,rY,sZ,S,T)),(No_omega^ yz))) - (Sum ((Sum (((y | Y) /^ (succ Y1)),((z | Z) /^ (succ Z1)),yz,(rY /^ (succ Y1)),(sZ /^ (succ Z1)),S,T)),(No_omega^ yz))) by A34, SURREALO:4; :: thesis: verum
end;
A36: ( y .. Y1 = y . Y1 & z .. Z1 = z . Z1 ) by A5, A15, Def5;
A37: |.(((SuY - (Sum ((r | (succ Y1)),((No_omega^ y) | (succ Y1))))) * ((uReal . ez) * (No_omega^ (z .. Z1)))) + ((SuZ - (Sum ((s | (succ Z1)),((No_omega^ z) | (succ Z1))))) * ((uReal . ey) * (No_omega^ (y .. Y1))))).| infinitely< No_omega^ ((y .. Y1) + (z .. Z1))
proof
( succ Y1 c= Y & Y c= (dom r) /\ (dom y) ) by A7, A15, ORDINAL1:28, ORDINAL1:def 2, A5, A2;
then A38: |.(((Sum (rY,((No_omega^ y) | Y))) - (Sum ((r | (succ Y1)),((No_omega^ y) | (succ Y1))))) * ((uReal . ez) * (No_omega^ (z .. Z1)))).| infinitely< No_omega^ ((y .. Y1) + (z .. Z1)) by Th104, A27;
(Sum (rY,((No_omega^ y) | Y))) - (Sum ((r | (succ Y1)),((No_omega^ y) | (succ Y1)))) == SuY - (Sum ((r | (succ Y1)),((No_omega^ y) | (succ Y1)))) by A10, Th28;
then ((Sum (rY,((No_omega^ y) | Y))) - (Sum ((r | (succ Y1)),((No_omega^ y) | (succ Y1))))) * ((uReal . ez) * (No_omega^ (z .. Z1))) == (SuY - (Sum ((r | (succ Y1)),((No_omega^ y) | (succ Y1))))) * ((uReal . ez) * (No_omega^ (z .. Z1))) by Th29;
then A39: |.((SuY - (Sum ((r | (succ Y1)),((No_omega^ y) | (succ Y1))))) * ((uReal . ez) * (No_omega^ (z .. Z1)))).| infinitely< No_omega^ ((y .. Y1) + (z .. Z1)) by A38, SURREALC:17, SURREALC:48;
( succ Z1 c= Z & Z c= (dom s) /\ (dom z) ) by ORDINAL1:def 2, A7, A15, ORDINAL1:28, A5, A2;
then A40: |.(((Sum (sZ,((No_omega^ z) | Z))) - (Sum ((s | (succ Z1)),((No_omega^ z) | (succ Z1))))) * ((uReal . ey) * (No_omega^ (y .. Y1)))).| infinitely< No_omega^ ((y .. Y1) + (z .. Z1)) by Th104, A28;
(Sum (sZ,((No_omega^ z) | Z))) - (Sum ((s | (succ Z1)),((No_omega^ z) | (succ Z1)))) == SuZ - (Sum ((s | (succ Z1)),((No_omega^ z) | (succ Z1)))) by A11, Th28;
then ((Sum (sZ,((No_omega^ z) | Z))) - (Sum ((s | (succ Z1)),((No_omega^ z) | (succ Z1))))) * ((uReal . ey) * (No_omega^ (y .. Y1))) == (SuZ - (Sum ((s | (succ Z1)),((No_omega^ z) | (succ Z1))))) * ((uReal . ey) * (No_omega^ (y .. Y1))) by Th29;
then |.((SuZ - (Sum ((s | (succ Z1)),((No_omega^ z) | (succ Z1))))) * ((uReal . ey) * (No_omega^ (y .. Y1)))).| infinitely< No_omega^ ((y .. Y1) + (z .. Z1)) by A40, SURREALC:17, SURREALC:48;
hence |.(((SuY - (Sum ((r | (succ Y1)),((No_omega^ y) | (succ Y1))))) * ((uReal . ez) * (No_omega^ (z .. Z1)))) + ((SuZ - (Sum ((s | (succ Z1)),((No_omega^ z) | (succ Z1))))) * ((uReal . ey) * (No_omega^ (y .. Y1))))).| infinitely< No_omega^ ((y .. Y1) + (z .. Z1)) by A39, SURREALC:41; :: thesis: verum
end;
A41: ( (y | Y) .. (succ Y1) = (y | Y) . (succ Y1) & (y | Y) . (succ Y1) = y . (succ Y1) & y . (succ Y1) = y .. (succ Y1) & (z | Z) .. (succ Z1) = (z | Z) . (succ Z1) & (z | Z) . (succ Z1) = z . (succ Z1) & z . (succ Z1) = z .. (succ Z1) ) by A5, A6, A20, A23, Def5, FUNCT_1:47;
then ( (y | Y) .. (succ Y1) < y .. Y1 & (z | Z) .. (succ Z1) <= z .. Z1 ) by ORDINAL1:6, A5, A20, A23, A36, SURREALC:def 11;
then A42: ((y | Y) .. (succ Y1)) + ((z | Z) .. (succ Z1)) < (y .. Y1) + (z .. Z1) by SURREALR:44;
A43: ( dom (y | Y) c= S & dom (z | Z) c= T ) by A5, A1, A6;
A44: |.(Sum ((Sum (((y | Y) /^ (succ Y1)),((z | Z) /^ (succ Z1)),yz,(rY /^ (succ Y1)),(sZ /^ (succ Z1)),S,T)),(No_omega^ yz))).| infinitely< No_omega^ ((y .. Y1) + (z .. Z1)) by A43, A12, A20, A23, A6, A42, Th108;
set sO1 = succ O1;
A45: ( dom (Sum ((y | Y),(z | Z),Uyz,rY,sZ,S,T)) = dom Uyz & dom (No_omega^ Uyz) = dom Uyz ) by Def19, SURREALC:def 22;
then succ O1 c= (dom (Sum ((y | Y),(z | Z),Uyz,rY,sZ,S,T))) /\ (dom (No_omega^ Uyz)) by A17, ORDINAL1:21;
then A46: Sum ((Sum ((y | Y),(z | Z),Uyz,rY,sZ,S,T)),(No_omega^ Uyz)) == (Sum (((Sum ((y | Y),(z | Z),Uyz,rY,sZ,S,T)) | (succ O1)),((No_omega^ Uyz) | (succ O1)))) + (Sum (((Sum ((y | Y),(z | Z),Uyz,rY,sZ,S,T)) /^ (succ O1)),((No_omega^ Uyz) /^ (succ O1)))) by Th71;
take APR = ((Sum (((Sum ((y | Y),(z | Z),Uyz,rY,sZ,S,T)) /^ (succ O1)),((No_omega^ Uyz) /^ (succ O1)))) + (- (Sum ((Sum (((y | Y) /^ (succ Y1)),((z | Z) /^ (succ Z1)),yz,(rY /^ (succ Y1)),(sZ /^ (succ Z1)),S,T)),(No_omega^ yz))))) + (((SuY - (Sum ((r | (succ Y1)),((No_omega^ y) | (succ Y1))))) * ((uReal . ez) * (No_omega^ (z .. Z1)))) + ((SuZ - (Sum ((s | (succ Z1)),((No_omega^ z) | (succ Z1))))) * ((uReal . ey) * (No_omega^ (y .. Y1))))); :: thesis: ( |.APR.| infinitely< No_omega^ ((y .. Y1) + (z .. Z1)) & ((SuY * z1) + (y1 * SuZ)) - (z1 * y1) == ((Sum (((Sum ((y | Y),(z | Z),Uyz,rY,sZ,S,T)) | (succ O1)),((No_omega^ Uyz) | (succ O1)))) + APR) - ((uReal . (ey * ez)) * (No_omega^ ((y .. Y1) + (z .. Z1)))) )
A47: succ O1 in dom Uyz
proof
( (y | Y) .. (succ Y1) in rng (y | Y) & (z | Z) .. (succ Z1) in rng (z | Z) ) by A20, A23, A6, A41, FUNCT_1:def 3;
then ((y | Y) .. (succ Y1)) + ((z | Z) .. (succ Z1)) in (rng (y | Y)) ++ (rng (z | Z)) by SURREALR:def 8;
then Unique_No (((y | Y) .. (succ Y1)) + ((z | Z) .. (succ Z1))) in rng Uyz by A8, Def8;
then consider d being object such that
A48: ( d in dom Uyz & Uyz . d = Unique_No (((y | Y) .. (succ Y1)) + ((z | Z) .. (succ Z1))) ) by FUNCT_1:def 3;
reconsider d = d as Ordinal by A48;
A49: Uyz . d = Uyz .. d by A48, Def5;
A50: Uyz .. O1 = Uyz . O1 by A17, Def5;
Unique_No (((y | Y) .. (succ Y1)) + ((z | Z) .. (succ Z1))) == ((y | Y) .. (succ Y1)) + ((z | Z) .. (succ Z1)) by SURREALO:def 10;
then A51: Uyz .. d == ((y | Y) .. (succ Y1)) + ((z | Z) .. (succ Z1)) by A48, Def5;
then Uyz .. d < (y .. Y1) + (z .. Z1) by A42, SURREALO:4;
then Uyz .. d <= Uyz .. O1 by A17, SURREALO:4;
then not d in O1 by A17, A49, A50, SURREALC:def 11;
then O1 c< d by A51, A17, ORDINAL1:16, A42, SURREALO:4;
then succ O1 c= d by ORDINAL1:11, ORDINAL1:21;
hence succ O1 in dom Uyz by A48, ORDINAL1:12; :: thesis: verum
end;
A52: O1 in succ O1 by ORDINAL1:6;
A53: ( Uyz .. (succ O1) = Uyz . (succ O1) & Uyz .. O1 = Uyz . O1 ) by A17, A47, Def5;
A54: ( 0 = (succ O1) -^ (succ O1) & (succ O1) -^ (succ O1) in (dom (Sum ((y | Y),(z | Z),Uyz,rY,sZ,S,T))) -^ (succ O1) ) by A47, A45, ORDINAL3:53, ORDINAL3:54;
A55: ( dom ((Sum ((y | Y),(z | Z),Uyz,rY,sZ,S,T)) /^ (succ O1)) = (dom (Sum ((y | Y),(z | Z),Uyz,rY,sZ,S,T))) -^ (succ O1) & dom ((No_omega^ Uyz) /^ (succ O1)) = (dom (No_omega^ Uyz)) -^ (succ O1) ) by Def1;
then A56: 0 in (dom ((Sum ((y | Y),(z | Z),Uyz,rY,sZ,S,T)) /^ (succ O1))) /\ (dom ((No_omega^ Uyz) /^ (succ O1))) by A45, A54;
A57: Uyz .. (succ O1) < (y .. Y1) + (z .. Z1) by A17, A53, A47, A52, SURREALC:def 11, SURREALO:4;
(succ O1) +^ 0 = succ O1 by ORDINAL2:27;
then A58: ( ((No_omega^ Uyz) /^ (succ O1)) .. 0 = ((No_omega^ Uyz) /^ (succ O1)) . 0 & ((No_omega^ Uyz) /^ (succ O1)) . 0 = (No_omega^ Uyz) . (succ O1) ) by A47, A45, A55, Def5, Th8;
Uyz . (succ O1) = Uyz .. (succ O1) by A47, Def5;
then ((No_omega^ Uyz) /^ (succ O1)) .. 0 = No_omega^ (Uyz .. (succ O1)) by A58, A45, A47, SURREALC:def 22;
then |.(Sum (((Sum ((y | Y),(z | Z),Uyz,rY,sZ,S,T)) /^ (succ O1)),((No_omega^ Uyz) /^ (succ O1)))).| infinitely< No_omega^ ((y .. Y1) + (z .. Z1)) by A56, A57, Th70, SURREALC:25;
then |.((Sum (((Sum ((y | Y),(z | Z),Uyz,rY,sZ,S,T)) /^ (succ O1)),((No_omega^ Uyz) /^ (succ O1)))) - (Sum ((Sum (((y | Y) /^ (succ Y1)),((z | Z) /^ (succ Z1)),yz,(rY /^ (succ Y1)),(sZ /^ (succ Z1)),S,T)),(No_omega^ yz)))).| infinitely< No_omega^ ((y .. Y1) + (z .. Z1)) by A44, SURREALC:43;
hence |.APR.| infinitely< No_omega^ ((y .. Y1) + (z .. Z1)) by A37, SURREALC:41; :: thesis: ((SuY * z1) + (y1 * SuZ)) - (z1 * y1) == ((Sum (((Sum ((y | Y),(z | Z),Uyz,rY,sZ,S,T)) | (succ O1)),((No_omega^ Uyz) | (succ O1)))) + APR) - ((uReal . (ey * ez)) * (No_omega^ ((y .. Y1) + (z .. Z1))))
(Sum ((Sum ((y | Y),(z | Z),yz,rY,sZ,S,T)),(No_omega^ yz))) - (Sum ((Sum (((y | Y) /^ (succ Y1)),((z | Z) /^ (succ Z1)),yz,(rY /^ (succ Y1)),(sZ /^ (succ Z1)),S,T)),(No_omega^ yz))) == ((Sum (((Sum ((y | Y),(z | Z),Uyz,rY,sZ,S,T)) | (succ O1)),((No_omega^ Uyz) | (succ O1)))) + (Sum (((Sum ((y | Y),(z | Z),Uyz,rY,sZ,S,T)) /^ (succ O1)),((No_omega^ Uyz) /^ (succ O1))))) - (Sum ((Sum (((y | Y) /^ (succ Y1)),((z | Z) /^ (succ Z1)),yz,(rY /^ (succ Y1)),(sZ /^ (succ Z1)),S,T)),(No_omega^ yz))) by A13, A46, SURREALR:66;
then ( ((SuY * (Sum ((s | (succ Z1)),((No_omega^ z) | (succ Z1))))) + ((Sum ((r | (succ Y1)),((No_omega^ y) | (succ Y1)))) * SuZ)) - ((Sum ((r | (succ Y1)),((No_omega^ y) | (succ Y1)))) * (Sum ((s | (succ Z1)),((No_omega^ z) | (succ Z1))))) == ((Sum (((Sum ((y | Y),(z | Z),Uyz,rY,sZ,S,T)) | (succ O1)),((No_omega^ Uyz) | (succ O1)))) + (Sum (((Sum ((y | Y),(z | Z),Uyz,rY,sZ,S,T)) /^ (succ O1)),((No_omega^ Uyz) /^ (succ O1))))) + (- (Sum ((Sum (((y | Y) /^ (succ Y1)),((z | Z) /^ (succ Z1)),yz,(rY /^ (succ Y1)),(sZ /^ (succ Z1)),S,T)),(No_omega^ yz)))) & ((Sum (((Sum ((y | Y),(z | Z),Uyz,rY,sZ,S,T)) | (succ O1)),((No_omega^ Uyz) | (succ O1)))) + (Sum (((Sum ((y | Y),(z | Z),Uyz,rY,sZ,S,T)) /^ (succ O1)),((No_omega^ Uyz) /^ (succ O1))))) + (- (Sum ((Sum (((y | Y) /^ (succ Y1)),((z | Z) /^ (succ Z1)),yz,(rY /^ (succ Y1)),(sZ /^ (succ Z1)),S,T)),(No_omega^ yz)))) = (Sum (((Sum ((y | Y),(z | Z),Uyz,rY,sZ,S,T)) | (succ O1)),((No_omega^ Uyz) | (succ O1)))) + ((Sum (((Sum ((y | Y),(z | Z),Uyz,rY,sZ,S,T)) /^ (succ O1)),((No_omega^ Uyz) /^ (succ O1)))) + (- (Sum ((Sum (((y | Y) /^ (succ Y1)),((z | Z) /^ (succ Z1)),yz,(rY /^ (succ Y1)),(sZ /^ (succ Z1)),S,T)),(No_omega^ yz))))) ) by A29, SURREALO:4, SURREALR:37;
then A59: ( (((SuY * (Sum ((s | (succ Z1)),((No_omega^ z) | (succ Z1))))) + ((Sum ((r | (succ Y1)),((No_omega^ y) | (succ Y1)))) * SuZ)) - ((Sum ((r | (succ Y1)),((No_omega^ y) | (succ Y1)))) * (Sum ((s | (succ Z1)),((No_omega^ z) | (succ Z1)))))) + (((SuY - (Sum ((r | (succ Y1)),((No_omega^ y) | (succ Y1))))) * ((uReal . ez) * (No_omega^ (z .. Z1)))) + ((SuZ - (Sum ((s | (succ Z1)),((No_omega^ z) | (succ Z1))))) * ((uReal . ey) * (No_omega^ (y .. Y1))))) == ((Sum (((Sum ((y | Y),(z | Z),Uyz,rY,sZ,S,T)) | (succ O1)),((No_omega^ Uyz) | (succ O1)))) + ((Sum (((Sum ((y | Y),(z | Z),Uyz,rY,sZ,S,T)) /^ (succ O1)),((No_omega^ Uyz) /^ (succ O1)))) + (- (Sum ((Sum (((y | Y) /^ (succ Y1)),((z | Z) /^ (succ Z1)),yz,(rY /^ (succ Y1)),(sZ /^ (succ Z1)),S,T)),(No_omega^ yz)))))) + (((SuY - (Sum ((r | (succ Y1)),((No_omega^ y) | (succ Y1))))) * ((uReal . ez) * (No_omega^ (z .. Z1)))) + ((SuZ - (Sum ((s | (succ Z1)),((No_omega^ z) | (succ Z1))))) * ((uReal . ey) * (No_omega^ (y .. Y1))))) & ((Sum (((Sum ((y | Y),(z | Z),Uyz,rY,sZ,S,T)) | (succ O1)),((No_omega^ Uyz) | (succ O1)))) + ((Sum (((Sum ((y | Y),(z | Z),Uyz,rY,sZ,S,T)) /^ (succ O1)),((No_omega^ Uyz) /^ (succ O1)))) + (- (Sum ((Sum (((y | Y) /^ (succ Y1)),((z | Z) /^ (succ Z1)),yz,(rY /^ (succ Y1)),(sZ /^ (succ Z1)),S,T)),(No_omega^ yz)))))) + (((SuY - (Sum ((r | (succ Y1)),((No_omega^ y) | (succ Y1))))) * ((uReal . ez) * (No_omega^ (z .. Z1)))) + ((SuZ - (Sum ((s | (succ Z1)),((No_omega^ z) | (succ Z1))))) * ((uReal . ey) * (No_omega^ (y .. Y1))))) = (Sum (((Sum ((y | Y),(z | Z),Uyz,rY,sZ,S,T)) | (succ O1)),((No_omega^ Uyz) | (succ O1)))) + APR ) by SURREALR:66, SURREALR:37;
(No_omega^ (z .. Z1)) * (No_omega^ (y .. Y1)) == No_omega^ ((y .. Y1) + (z .. Z1)) by SURREALC:27;
then ((uReal . ez) * (No_omega^ (z .. Z1))) * ((uReal . ey) * (No_omega^ (y .. Y1))) == (uReal . (ey * ez)) * (No_omega^ ((y .. Y1) + (z .. Z1))) by Lm6;
then ((((SuY * (Sum ((s | (succ Z1)),((No_omega^ z) | (succ Z1))))) + ((Sum ((r | (succ Y1)),((No_omega^ y) | (succ Y1)))) * SuZ)) - ((Sum ((r | (succ Y1)),((No_omega^ y) | (succ Y1)))) * (Sum ((s | (succ Z1)),((No_omega^ z) | (succ Z1)))))) + (((SuY - (Sum ((r | (succ Y1)),((No_omega^ y) | (succ Y1))))) * ((uReal . ez) * (No_omega^ (z .. Z1)))) + ((SuZ - (Sum ((s | (succ Z1)),((No_omega^ z) | (succ Z1))))) * ((uReal . ey) * (No_omega^ (y .. Y1)))))) - (((uReal . ez) * (No_omega^ (z .. Z1))) * ((uReal . ey) * (No_omega^ (y .. Y1)))) == ((Sum (((Sum ((y | Y),(z | Z),Uyz,rY,sZ,S,T)) | (succ O1)),((No_omega^ Uyz) | (succ O1)))) + APR) - ((uReal . (ey * ez)) * (No_omega^ ((y .. Y1) + (z .. Z1)))) by A59, Th28;
hence ((SuY * z1) + (y1 * SuZ)) - (z1 * y1) == ((Sum (((Sum ((y | Y),(z | Z),Uyz,rY,sZ,S,T)) | (succ O1)),((No_omega^ Uyz) | (succ O1)))) + APR) - ((uReal . (ey * ez)) * (No_omega^ ((y .. Y1) + (z .. Z1)))) by A19, SURREALO:4; :: thesis: verum
end;
set D = dom Uyz;
A60: ( dom (No_omega^ Uyz) = dom Uyz & dom Uyz = dom (Sum ((y | Y),(z | Z),Uyz,rY,sZ,S,T)) ) by Def19, SURREALC:def 22;
then A61: dom Uyz c= (dom (Sum ((y | Y),(z | Z),Uyz,rY,sZ,S,T))) /\ (dom (No_omega^ Uyz)) ;
reconsider SUP = [ { ((Sum (((Sum ((y | Y),(z | Z),Uyz,rY,sZ,S,T)) | B),((No_omega^ Uyz) | B))) + ((uReal . (((Sum ((y | Y),(z | Z),Uyz,rY,sZ,S,T)) . B) - e)) * ((No_omega^ Uyz) .. B))) where B is Element of dom Uyz, e is positive Real : B in dom Uyz } , { ((Sum (((Sum ((y | Y),(z | Z),Uyz,rY,sZ,S,T)) | B),((No_omega^ Uyz) | B))) + ((uReal . (((Sum ((y | Y),(z | Z),Uyz,rY,sZ,S,T)) . B) + e)) * ((No_omega^ Uyz) .. B))) where B is Element of dom Uyz, e is positive Real : B in dom Uyz } ] as Surreal by A61, Th61;
Unique_No SUP = Sum (((Sum ((y | Y),(z | Z),Uyz,rY,sZ,S,T)) | (dom Uyz)),((No_omega^ Uyz) | (dom Uyz))) by A61, Th62;
then A62: SUP == Sum (((Sum ((y | Y),(z | Z),Uyz,rY,sZ,S,T)) | (dom Uyz)),((No_omega^ Uyz) | (dom Uyz))) by SURREALO:def 10;
A63: SuY * SuZ = [((comp ((L_ SuY),SuY,SuZ,(L_ SuZ))) \/ (comp ((R_ SuY),SuY,SuZ,(R_ SuZ)))),((comp ((L_ SuY),SuY,SuZ,(R_ SuZ))) \/ (comp ((R_ SuY),SuY,SuZ,(L_ SuZ))))] by SURREALR:50;
A64: for Y1, Z1 being Ordinal st Y1 in Y & Z1 in Z holds
ex O1 being Ordinal st
( O1 in dom Uyz & Uyz .. O1 == (y .. Y1) + (z .. Z1) )
proof
let Y1, Z1 be Ordinal; :: thesis: ( Y1 in Y & Z1 in Z implies ex O1 being Ordinal st
( O1 in dom Uyz & Uyz .. O1 == (y .. Y1) + (z .. Z1) ) )
assume A65: ( Y1 in Y & Z1 in Z ) ; :: thesis: ex O1 being Ordinal st
( O1 in dom Uyz & Uyz .. O1 == (y .. Y1) + (z .. Z1) )
A66: ( y .. Y1 = y . Y1 & y . Y1 = (y | Y) . Y1 & z .. Z1 = z . Z1 & z . Z1 = (z | Z) . Z1 ) by A65, A6, Def5, A5, FUNCT_1:47;
( y .. Y1 in rng (y | Y) & z .. Z1 in rng (z | Z) ) by A65, A6, A66, FUNCT_1:def 3;
then (y .. Y1) + (z .. Z1) in (rng (y | Y)) ++ (rng (z | Z)) by SURREALR:def 8;
then Unique_No ((y .. Y1) + (z .. Z1)) in rng Uyz by A8, Def8;
then consider d being object such that
A67: ( d in dom Uyz & Uyz . d = Unique_No ((y .. Y1) + (z .. Z1)) ) by FUNCT_1:def 3;
reconsider d = d as Ordinal by A67;
take d ; :: thesis: ( d in dom Uyz & Uyz .. d == (y .. Y1) + (z .. Z1) )
Unique_No ((y .. Y1) + (z .. Z1)) == (y .. Y1) + (z .. Z1) by SURREALO:def 10;
hence ( d in dom Uyz & Uyz .. d == (y .. Y1) + (z .. Z1) ) by A67, Def5; :: thesis: verum
end;
A68: for ll being Surreal st ll in L_ (SuY * SuZ) holds
ex rr being Surreal st
( rr in L_ SUP & ll <= rr )
proof
let ll be Surreal; :: thesis: ( ll in L_ (SuY * SuZ) implies ex rr being Surreal st
( rr in L_ SUP & ll <= rr ) )
assume A69: ll in L_ (SuY * SuZ) ; :: thesis: ex rr being Surreal st
( rr in L_ SUP & ll <= rr )
per cases ( ll in comp ((L_ SuY),SuY,SuZ,(L_ SuZ)) or ll in comp ((R_ SuY),SuY,SuZ,(R_ SuZ)) ) by A63, A69, XBOOLE_0:def 3;
suppose ll in comp ((L_ SuY),SuY,SuZ,(L_ SuZ)) ; :: thesis: ex rr being Surreal st
( rr in L_ SUP & ll <= rr )
then consider a1, b1 being Surreal such that
A70: ( ll = ((a1 * SuZ) + (SuY * b1)) - (a1 * b1) & a1 in L_ SuY & b1 in L_ SuZ ) by SURREALR:def 15;
consider Y1 being Element of Y, ey being positive Real such that
A71: ( a1 = (Sum ((r | Y1),((No_omega^ y) | Y1))) + ((uReal . ((r . Y1) - ey)) * ((No_omega^ y) .. Y1)) & Y1 in Y ) by A70;
consider Z1 being Element of Z, ez being positive Real such that
A72: ( b1 = (Sum ((s | Z1),((No_omega^ z) | Z1))) + ((uReal . ((s . Z1) - ez)) * ((No_omega^ z) .. Z1)) & Z1 in Z ) by A70;
set E = ey * ez;
succ Y1 c= (dom r) /\ (dom y) by A5, A2, A71, ORDINAL1:21;
then A73: a1 == (Sum ((r | (succ Y1)),((No_omega^ y) | (succ Y1)))) + ((uReal . (- ey)) * (No_omega^ (y .. Y1))) by A71, Th102;
succ Z1 c= (dom s) /\ (dom z) by A5, A2, A72, ORDINAL1:21;
then A74: b1 == (Sum ((s | (succ Z1)),((No_omega^ z) | (succ Z1)))) + ((uReal . (- ez)) * (No_omega^ (z .. Z1))) by A72, Th102;
consider O1 being Ordinal such that
A75: ( O1 in dom Uyz & Uyz .. O1 == (y .. Y1) + (z .. Z1) ) by A71, A72, A64;
set sO1 = succ O1;
take rr = (Sum (((Sum ((y | Y),(z | Z),Uyz,rY,sZ,S,T)) | O1),((No_omega^ Uyz) | O1))) + ((uReal . (((Sum ((y | Y),(z | Z),Uyz,rY,sZ,S,T)) . O1) - ((ey * ez) / 2))) * ((No_omega^ Uyz) .. O1)); :: thesis: ( rr in L_ SUP & ll <= rr )
thus rr in L_ SUP by A75; :: thesis: ll <= rr
set SS = Sum (((Sum ((y | Y),(z | Z),Uyz,rY,sZ,S,T)) | (succ O1)),((No_omega^ Uyz) | (succ O1)));
set NN = No_omega^ ((y .. Y1) + (z .. Z1));
consider T being Surreal such that
A76: |.T.| infinitely< No_omega^ ((y .. Y1) + (z .. Z1)) and
A77: ((SuY * b1) + (a1 * SuZ)) - (b1 * a1) == ((Sum (((Sum ((y | Y),(z | Z),Uyz,rY,sZ,S,T)) | (succ O1)),((No_omega^ Uyz) | (succ O1)))) + T) - ((uReal . ((- ey) * (- ez))) * (No_omega^ ((y .. Y1) + (z .. Z1)))) by A71, A72, A73, A74, A75, A14;
|.T.| infinitely< (uReal . ((ey * ez) / 2)) * (No_omega^ ((y .. Y1) + (z .. Z1))) by A76, SURREALC:13;
then ( T <= |.T.| & |.T.| < (uReal . ((ey * ez) / 2)) * (No_omega^ ((y .. Y1) + (z .. Z1))) ) by SURREALC:9, SURREALC:34;
then T < (uReal . ((ey * ez) / 2)) * (No_omega^ ((y .. Y1) + (z .. Z1))) by SURREALO:4;
then (Sum (((Sum ((y | Y),(z | Z),Uyz,rY,sZ,S,T)) | (succ O1)),((No_omega^ Uyz) | (succ O1)))) + T < (Sum (((Sum ((y | Y),(z | Z),Uyz,rY,sZ,S,T)) | (succ O1)),((No_omega^ Uyz) | (succ O1)))) + ((uReal . ((ey * ez) / 2)) * (No_omega^ ((y .. Y1) + (z .. Z1)))) by SURREALR:44;
then ( ((Sum (((Sum ((y | Y),(z | Z),Uyz,rY,sZ,S,T)) | (succ O1)),((No_omega^ Uyz) | (succ O1)))) + T) + (- ((uReal . (ey * ez)) * (No_omega^ ((y .. Y1) + (z .. Z1))))) < ((Sum (((Sum ((y | Y),(z | Z),Uyz,rY,sZ,S,T)) | (succ O1)),((No_omega^ Uyz) | (succ O1)))) + ((uReal . ((ey * ez) / 2)) * (No_omega^ ((y .. Y1) + (z .. Z1))))) - ((uReal . (ey * ez)) * (No_omega^ ((y .. Y1) + (z .. Z1)))) & ((Sum (((Sum ((y | Y),(z | Z),Uyz,rY,sZ,S,T)) | (succ O1)),((No_omega^ Uyz) | (succ O1)))) + ((uReal . ((ey * ez) / 2)) * (No_omega^ ((y .. Y1) + (z .. Z1))))) - ((uReal . (ey * ez)) * (No_omega^ ((y .. Y1) + (z .. Z1)))) == (Sum (((Sum ((y | Y),(z | Z),Uyz,rY,sZ,S,T)) | (succ O1)),((No_omega^ Uyz) | (succ O1)))) + ((uReal . (((ey * ez) / 2) - (ey * ez))) * (No_omega^ ((y .. Y1) + (z .. Z1)))) ) by Th30, SURREALR:44;
then ((Sum (((Sum ((y | Y),(z | Z),Uyz,rY,sZ,S,T)) | (succ O1)),((No_omega^ Uyz) | (succ O1)))) + T) + (- ((uReal . (ey * ez)) * (No_omega^ ((y .. Y1) + (z .. Z1))))) < (Sum (((Sum ((y | Y),(z | Z),Uyz,rY,sZ,S,T)) | (succ O1)),((No_omega^ Uyz) | (succ O1)))) + ((uReal . (- ((ey * ez) / 2))) * (No_omega^ ((y .. Y1) + (z .. Z1)))) by SURREALO:4;
then A78: ll < (Sum (((Sum ((y | Y),(z | Z),Uyz,rY,sZ,S,T)) | (succ O1)),((No_omega^ Uyz) | (succ O1)))) + ((uReal . (- ((ey * ez) / 2))) * (No_omega^ ((y .. Y1) + (z .. Z1)))) by A70, A77, SURREALO:4;
No_omega^ ((y .. Y1) + (z .. Z1)) == No_omega^ (Uyz .. O1) by A75, SURREALC:24;
then (uReal . (- ((ey * ez) / 2))) * (No_omega^ ((y .. Y1) + (z .. Z1))) == (uReal . (- ((ey * ez) / 2))) * (No_omega^ (Uyz .. O1)) by SURREALR:54;
then (Sum (((Sum ((y | Y),(z | Z),Uyz,rY,sZ,S,T)) | (succ O1)),((No_omega^ Uyz) | (succ O1)))) + ((uReal . (- ((ey * ez) / 2))) * (No_omega^ ((y .. Y1) + (z .. Z1)))) == (Sum (((Sum ((y | Y),(z | Z),Uyz,rY,sZ,S,T)) | (succ O1)),((No_omega^ Uyz) | (succ O1)))) + ((uReal . (- ((ey * ez) / 2))) * (No_omega^ (Uyz .. O1))) by SURREALR:66;
then A79: ll < (Sum (((Sum ((y | Y),(z | Z),Uyz,rY,sZ,S,T)) | (succ O1)),((No_omega^ Uyz) | (succ O1)))) + ((uReal . (- ((ey * ez) / 2))) * (No_omega^ (Uyz .. O1))) by A78, SURREALO:4;
succ O1 c= (dom (Sum ((y | Y),(z | Z),Uyz,rY,sZ,S,T))) /\ (dom Uyz) by A60, A75, ORDINAL1:21;
then (Sum (((Sum ((y | Y),(z | Z),Uyz,rY,sZ,S,T)) | (succ O1)),((No_omega^ Uyz) | (succ O1)))) + ((uReal . (- ((ey * ez) / 2))) * (No_omega^ (Uyz .. O1))) == rr by Th102;
hence ll <= rr by A79, SURREALO:4; :: thesis: verum
end;
suppose ll in comp ((R_ SuY),SuY,SuZ,(R_ SuZ)) ; :: thesis: ex rr being Surreal st
( rr in L_ SUP & ll <= rr )
then consider a1, b1 being Surreal such that
A80: ( ll = ((a1 * SuZ) + (SuY * b1)) - (a1 * b1) & a1 in R_ SuY & b1 in R_ SuZ ) by SURREALR:def 15;
consider Y1 being Element of Y, ey being positive Real such that
A81: ( a1 = (Sum ((r | Y1),((No_omega^ y) | Y1))) + ((uReal . ((r . Y1) + ey)) * ((No_omega^ y) .. Y1)) & Y1 in Y ) by A80;
consider Z1 being Element of Z, ez being positive Real such that
A82: ( b1 = (Sum ((s | Z1),((No_omega^ z) | Z1))) + ((uReal . ((s . Z1) + ez)) * ((No_omega^ z) .. Z1)) & Z1 in Z ) by A80;
set E = ey * ez;
succ Y1 c= (dom r) /\ (dom y) by A5, A2, A81, ORDINAL1:21;
then A83: a1 == (Sum ((r | (succ Y1)),((No_omega^ y) | (succ Y1)))) + ((uReal . ey) * (No_omega^ (y .. Y1))) by A81, Th102;
succ Z1 c= (dom s) /\ (dom z) by A5, A2, A82, ORDINAL1:21;
then A84: b1 == (Sum ((s | (succ Z1)),((No_omega^ z) | (succ Z1)))) + ((uReal . ez) * (No_omega^ (z .. Z1))) by A82, Th102;
consider O1 being Ordinal such that
A85: ( O1 in dom Uyz & Uyz .. O1 == (y .. Y1) + (z .. Z1) ) by A81, A82, A64;
set sO1 = succ O1;
take rr = (Sum (((Sum ((y | Y),(z | Z),Uyz,rY,sZ,S,T)) | O1),((No_omega^ Uyz) | O1))) + ((uReal . (((Sum ((y | Y),(z | Z),Uyz,rY,sZ,S,T)) . O1) - ((ey * ez) / 2))) * ((No_omega^ Uyz) .. O1)); :: thesis: ( rr in L_ SUP & ll <= rr )
thus rr in L_ SUP by A85; :: thesis: ll <= rr
set SS = Sum (((Sum ((y | Y),(z | Z),Uyz,rY,sZ,S,T)) | (succ O1)),((No_omega^ Uyz) | (succ O1)));
set NN = No_omega^ ((y .. Y1) + (z .. Z1));
consider T being Surreal such that
A86: |.T.| infinitely< No_omega^ ((y .. Y1) + (z .. Z1)) and
A87: ((SuY * b1) + (a1 * SuZ)) - (b1 * a1) == ((Sum (((Sum ((y | Y),(z | Z),Uyz,rY,sZ,S,T)) | (succ O1)),((No_omega^ Uyz) | (succ O1)))) + T) - ((uReal . (ey * ez)) * (No_omega^ ((y .. Y1) + (z .. Z1)))) by A81, A82, A83, A84, A85, A14;
|.T.| infinitely< (uReal . ((ey * ez) / 2)) * (No_omega^ ((y .. Y1) + (z .. Z1))) by A86, SURREALC:13;
then ( T <= |.T.| & |.T.| < (uReal . ((ey * ez) / 2)) * (No_omega^ ((y .. Y1) + (z .. Z1))) ) by SURREALC:9, SURREALC:34;
then T < (uReal . ((ey * ez) / 2)) * (No_omega^ ((y .. Y1) + (z .. Z1))) by SURREALO:4;
then (Sum (((Sum ((y | Y),(z | Z),Uyz,rY,sZ,S,T)) | (succ O1)),((No_omega^ Uyz) | (succ O1)))) + T < (Sum (((Sum ((y | Y),(z | Z),Uyz,rY,sZ,S,T)) | (succ O1)),((No_omega^ Uyz) | (succ O1)))) + ((uReal . ((ey * ez) / 2)) * (No_omega^ ((y .. Y1) + (z .. Z1)))) by SURREALR:44;
then ( ((Sum (((Sum ((y | Y),(z | Z),Uyz,rY,sZ,S,T)) | (succ O1)),((No_omega^ Uyz) | (succ O1)))) + T) + (- ((uReal . (ey * ez)) * (No_omega^ ((y .. Y1) + (z .. Z1))))) < ((Sum (((Sum ((y | Y),(z | Z),Uyz,rY,sZ,S,T)) | (succ O1)),((No_omega^ Uyz) | (succ O1)))) + ((uReal . ((ey * ez) / 2)) * (No_omega^ ((y .. Y1) + (z .. Z1))))) - ((uReal . (ey * ez)) * (No_omega^ ((y .. Y1) + (z .. Z1)))) & ((Sum (((Sum ((y | Y),(z | Z),Uyz,rY,sZ,S,T)) | (succ O1)),((No_omega^ Uyz) | (succ O1)))) + ((uReal . ((ey * ez) / 2)) * (No_omega^ ((y .. Y1) + (z .. Z1))))) - ((uReal . (ey * ez)) * (No_omega^ ((y .. Y1) + (z .. Z1)))) == (Sum (((Sum ((y | Y),(z | Z),Uyz,rY,sZ,S,T)) | (succ O1)),((No_omega^ Uyz) | (succ O1)))) + ((uReal . (((ey * ez) / 2) - (ey * ez))) * (No_omega^ ((y .. Y1) + (z .. Z1)))) ) by Th30, SURREALR:44;
then ((Sum (((Sum ((y | Y),(z | Z),Uyz,rY,sZ,S,T)) | (succ O1)),((No_omega^ Uyz) | (succ O1)))) + T) + (- ((uReal . (ey * ez)) * (No_omega^ ((y .. Y1) + (z .. Z1))))) < (Sum (((Sum ((y | Y),(z | Z),Uyz,rY,sZ,S,T)) | (succ O1)),((No_omega^ Uyz) | (succ O1)))) + ((uReal . (- ((ey * ez) / 2))) * (No_omega^ ((y .. Y1) + (z .. Z1)))) by SURREALO:4;
then A88: ll < (Sum (((Sum ((y | Y),(z | Z),Uyz,rY,sZ,S,T)) | (succ O1)),((No_omega^ Uyz) | (succ O1)))) + ((uReal . (- ((ey * ez) / 2))) * (No_omega^ ((y .. Y1) + (z .. Z1)))) by A80, A87, SURREALO:4;
No_omega^ ((y .. Y1) + (z .. Z1)) == No_omega^ (Uyz .. O1) by A85, SURREALC:24;
then (uReal . (- ((ey * ez) / 2))) * (No_omega^ ((y .. Y1) + (z .. Z1))) == (uReal . (- ((ey * ez) / 2))) * (No_omega^ (Uyz .. O1)) by SURREALR:54;
then (Sum (((Sum ((y | Y),(z | Z),Uyz,rY,sZ,S,T)) | (succ O1)),((No_omega^ Uyz) | (succ O1)))) + ((uReal . (- ((ey * ez) / 2))) * (No_omega^ ((y .. Y1) + (z .. Z1)))) == (Sum (((Sum ((y | Y),(z | Z),Uyz,rY,sZ,S,T)) | (succ O1)),((No_omega^ Uyz) | (succ O1)))) + ((uReal . (- ((ey * ez) / 2))) * (No_omega^ (Uyz .. O1))) by SURREALR:66;
then A89: ll < (Sum (((Sum ((y | Y),(z | Z),Uyz,rY,sZ,S,T)) | (succ O1)),((No_omega^ Uyz) | (succ O1)))) + ((uReal . (- ((ey * ez) / 2))) * (No_omega^ (Uyz .. O1))) by A88, SURREALO:4;
succ O1 c= (dom (Sum ((y | Y),(z | Z),Uyz,rY,sZ,S,T))) /\ (dom Uyz) by A60, A85, ORDINAL1:21;
then (Sum (((Sum ((y | Y),(z | Z),Uyz,rY,sZ,S,T)) | (succ O1)),((No_omega^ Uyz) | (succ O1)))) + ((uReal . (- ((ey * ez) / 2))) * (No_omega^ (Uyz .. O1))) == rr by Th102;
hence ll <= rr by A89, SURREALO:4; :: thesis: verum
end;
end;
end;
A90: for O1 being Ordinal st O1 in dom Uyz holds
ex Y1, Z1 being Ordinal st
( Y1 in Y & Z1 in Z & Uyz .. O1 == (y .. Y1) + (z .. Z1) )
proof
let O1 be Ordinal; :: thesis: ( O1 in dom Uyz implies ex Y1, Z1 being Ordinal st
( Y1 in Y & Z1 in Z & Uyz .. O1 == (y .. Y1) + (z .. Z1) ) )
assume A91: O1 in dom Uyz ; :: thesis: ex Y1, Z1 being Ordinal st
( Y1 in Y & Z1 in Z & Uyz .. O1 == (y .. Y1) + (z .. Z1) )
Uyz . O1 = Uyz .. O1 by A91, Def5;
then Uyz .. O1 in Unique_No ((rng (y | Y)) ++ (rng (z | Z))) by A8, A91, FUNCT_1:def 3;
then consider d being Surreal such that
A92: ( d in (rng (y | Y)) ++ (rng (z | Z)) & Unique_No d = Uyz .. O1 ) by Def8;
consider i, j being Surreal such that
A93: ( i in rng (y | Y) & j in rng (z | Z) & d = i + j ) by A92, SURREALR:def 8;
consider Y1 being object such that
A94: ( Y1 in dom (y | Y) & (y | Y) . Y1 = i ) by A93, FUNCT_1:def 3;
consider Z1 being object such that
A95: ( Z1 in dom (z | Z) & (z | Z) . Z1 = j ) by A93, FUNCT_1:def 3;
reconsider Y1 = Y1, Z1 = Z1 as Ordinal by A94, A95;
take Y1 ; :: thesis: ex Z1 being Ordinal st
( Y1 in Y & Z1 in Z & Uyz .. O1 == (y .. Y1) + (z .. Z1) )
take Z1 ; :: thesis: ( Y1 in Y & Z1 in Z & Uyz .. O1 == (y .. Y1) + (z .. Z1) )
thus ( Y1 in Y & Z1 in Z ) by A94, A95, A5, RELAT_1:62; :: thesis: Uyz .. O1 == (y .. Y1) + (z .. Z1)
( y .. Y1 = y . Y1 & y . Y1 = (y | Y) . Y1 & z .. Z1 = z . Z1 & z . Z1 = (z | Z) . Z1 ) by A94, A95, Def5, A5, A6, FUNCT_1:47;
hence Uyz .. O1 == (y .. Y1) + (z .. Z1) by A92, A93, A94, A95, SURREALO:def 10; :: thesis: verum
end;
A96: for ll being Surreal st ll in R_ SUP holds
ex rr being Surreal st
( rr in R_ (SuY * SuZ) & rr <= ll )
proof
let ll be Surreal; :: thesis: ( ll in R_ SUP implies ex rr being Surreal st
( rr in R_ (SuY * SuZ) & rr <= ll ) )
assume A97: ll in R_ SUP ; :: thesis: ex rr being Surreal st
( rr in R_ (SuY * SuZ) & rr <= ll )
consider O1 being Element of dom Uyz, e being positive Real such that
A98: ( ll = (Sum (((Sum ((y | Y),(z | Z),Uyz,rY,sZ,S,T)) | O1),((No_omega^ Uyz) | O1))) + ((uReal . (((Sum ((y | Y),(z | Z),Uyz,rY,sZ,S,T)) . O1) + e)) * ((No_omega^ Uyz) .. O1)) & O1 in dom Uyz ) by A97;
consider Y1, Z1 being Ordinal such that
A99: Y1 in Y and
A100: Z1 in Z and
A101: Uyz .. O1 == (y .. Y1) + (z .. Z1) by A90, A98;
set ey = e;
set ez = 1 / 2;
set E = e * (1 / 2);
set a1 = (Sum ((r | Y1),((No_omega^ y) | Y1))) + ((uReal . ((r . Y1) - e)) * ((No_omega^ y) .. Y1));
set b1 = (Sum ((s | Z1),((No_omega^ z) | Z1))) + ((uReal . ((s . Z1) + (1 / 2))) * ((No_omega^ z) .. Z1));
succ Y1 c= (dom r) /\ (dom y) by A5, A2, A99, ORDINAL1:21;
then A102: (Sum ((r | Y1),((No_omega^ y) | Y1))) + ((uReal . ((r . Y1) - e)) * ((No_omega^ y) .. Y1)) == (Sum ((r | (succ Y1)),((No_omega^ y) | (succ Y1)))) + ((uReal . (- e)) * (No_omega^ (y .. Y1))) by Th102;
succ Z1 c= (dom s) /\ (dom z) by A5, A2, A100, ORDINAL1:21;
then A103: (Sum ((s | Z1),((No_omega^ z) | Z1))) + ((uReal . ((s . Z1) + (1 / 2))) * ((No_omega^ z) .. Z1)) == (Sum ((s | (succ Z1)),((No_omega^ z) | (succ Z1)))) + ((uReal . (1 / 2)) * (No_omega^ (z .. Z1))) by Th102;
take rr = ((SuY * ((Sum ((s | Z1),((No_omega^ z) | Z1))) + ((uReal . ((s . Z1) + (1 / 2))) * ((No_omega^ z) .. Z1)))) + (((Sum ((r | Y1),((No_omega^ y) | Y1))) + ((uReal . ((r . Y1) - e)) * ((No_omega^ y) .. Y1))) * SuZ)) - (((Sum ((s | Z1),((No_omega^ z) | Z1))) + ((uReal . ((s . Z1) + (1 / 2))) * ((No_omega^ z) .. Z1))) * ((Sum ((r | Y1),((No_omega^ y) | Y1))) + ((uReal . ((r . Y1) - e)) * ((No_omega^ y) .. Y1)))); :: thesis: ( rr in R_ (SuY * SuZ) & rr <= ll )
set sO1 = succ O1;
set SS = Sum (((Sum ((y | Y),(z | Z),Uyz,rY,sZ,S,T)) | (succ O1)),((No_omega^ Uyz) | (succ O1)));
set NN = No_omega^ ((y .. Y1) + (z .. Z1));
consider T being Surreal such that
A104: |.T.| infinitely< No_omega^ ((y .. Y1) + (z .. Z1)) and
A105: rr == ((Sum (((Sum ((y | Y),(z | Z),Uyz,rY,sZ,S,T)) | (succ O1)),((No_omega^ Uyz) | (succ O1)))) + T) - ((uReal . ((- e) * (1 / 2))) * (No_omega^ ((y .. Y1) + (z .. Z1)))) by A98, A99, A100, A102, A103, A101, A14;
succ O1 c= (dom (Sum ((y | Y),(z | Z),Uyz,rY,sZ,S,T))) /\ (dom Uyz) by A60, A98, ORDINAL1:21;
then A106: (Sum (((Sum ((y | Y),(z | Z),Uyz,rY,sZ,S,T)) | (succ O1)),((No_omega^ Uyz) | (succ O1)))) + ((uReal . e) * (No_omega^ (Uyz .. O1))) == ll by Th102, A98;
( (Sum ((s | Z1),((No_omega^ z) | Z1))) + ((uReal . ((s . Z1) + (1 / 2))) * ((No_omega^ z) .. Z1)) in R_ SuZ & (Sum ((r | Y1),((No_omega^ y) | Y1))) + ((uReal . ((r . Y1) - e)) * ((No_omega^ y) .. Y1)) in L_ SuY ) by A99, A100;
then rr in comp ((L_ SuY),SuY,SuZ,(R_ SuZ)) by SURREALR:def 15;
hence rr in R_ (SuY * SuZ) by A63, XBOOLE_0:def 3; :: thesis: rr <= ll
|.T.| infinitely< (uReal . (e / 2)) * (No_omega^ ((y .. Y1) + (z .. Z1))) by A104, SURREALC:13;
then ( T <= |.T.| & |.T.| < (uReal . (e / 2)) * (No_omega^ ((y .. Y1) + (z .. Z1))) ) by SURREALC:9, SURREALC:34;
then T < (uReal . (e / 2)) * (No_omega^ ((y .. Y1) + (z .. Z1))) by SURREALO:4;
then (Sum (((Sum ((y | Y),(z | Z),Uyz,rY,sZ,S,T)) | (succ O1)),((No_omega^ Uyz) | (succ O1)))) + T < (Sum (((Sum ((y | Y),(z | Z),Uyz,rY,sZ,S,T)) | (succ O1)),((No_omega^ Uyz) | (succ O1)))) + ((uReal . (e / 2)) * (No_omega^ ((y .. Y1) + (z .. Z1)))) by SURREALR:44;
then ( ((Sum (((Sum ((y | Y),(z | Z),Uyz,rY,sZ,S,T)) | (succ O1)),((No_omega^ Uyz) | (succ O1)))) + T) + (- ((uReal . (- (e * (1 / 2)))) * (No_omega^ ((y .. Y1) + (z .. Z1))))) < ((Sum (((Sum ((y | Y),(z | Z),Uyz,rY,sZ,S,T)) | (succ O1)),((No_omega^ Uyz) | (succ O1)))) + ((uReal . (e / 2)) * (No_omega^ ((y .. Y1) + (z .. Z1))))) - ((uReal . (- (e * (1 / 2)))) * (No_omega^ ((y .. Y1) + (z .. Z1)))) & ((Sum (((Sum ((y | Y),(z | Z),Uyz,rY,sZ,S,T)) | (succ O1)),((No_omega^ Uyz) | (succ O1)))) + ((uReal . (e / 2)) * (No_omega^ ((y .. Y1) + (z .. Z1))))) - ((uReal . (- (e * (1 / 2)))) * (No_omega^ ((y .. Y1) + (z .. Z1)))) == (Sum (((Sum ((y | Y),(z | Z),Uyz,rY,sZ,S,T)) | (succ O1)),((No_omega^ Uyz) | (succ O1)))) + ((uReal . ((e / 2) - (- (e * (1 / 2))))) * (No_omega^ ((y .. Y1) + (z .. Z1)))) ) by Th30, SURREALR:44;
then ((Sum (((Sum ((y | Y),(z | Z),Uyz,rY,sZ,S,T)) | (succ O1)),((No_omega^ Uyz) | (succ O1)))) + T) + (- ((uReal . (- (e * (1 / 2)))) * (No_omega^ ((y .. Y1) + (z .. Z1))))) < (Sum (((Sum ((y | Y),(z | Z),Uyz,rY,sZ,S,T)) | (succ O1)),((No_omega^ Uyz) | (succ O1)))) + ((uReal . e) * (No_omega^ ((y .. Y1) + (z .. Z1)))) by SURREALO:4;
then A107: rr < (Sum (((Sum ((y | Y),(z | Z),Uyz,rY,sZ,S,T)) | (succ O1)),((No_omega^ Uyz) | (succ O1)))) + ((uReal . e) * (No_omega^ ((y .. Y1) + (z .. Z1)))) by A105, SURREALO:4;
No_omega^ ((y .. Y1) + (z .. Z1)) == No_omega^ (Uyz .. O1) by A101, SURREALC:24;
then (uReal . e) * (No_omega^ ((y .. Y1) + (z .. Z1))) == (uReal . e) * (No_omega^ (Uyz .. O1)) by SURREALR:54;
then (Sum (((Sum ((y | Y),(z | Z),Uyz,rY,sZ,S,T)) | (succ O1)),((No_omega^ Uyz) | (succ O1)))) + ((uReal . e) * (No_omega^ ((y .. Y1) + (z .. Z1)))) == (Sum (((Sum ((y | Y),(z | Z),Uyz,rY,sZ,S,T)) | (succ O1)),((No_omega^ Uyz) | (succ O1)))) + ((uReal . e) * (No_omega^ (Uyz .. O1))) by SURREALR:66;
then rr < (Sum (((Sum ((y | Y),(z | Z),Uyz,rY,sZ,S,T)) | (succ O1)),((No_omega^ Uyz) | (succ O1)))) + ((uReal . e) * (No_omega^ (Uyz .. O1))) by A107, SURREALO:4;
hence rr <= ll by A106, SURREALO:4; :: thesis: verum
end;
A108: for ll being Surreal st ll in R_ (SuY * SuZ) holds
ex rr being Surreal st
( rr in R_ SUP & rr <= ll )
proof
let ll be Surreal; :: thesis: ( ll in R_ (SuY * SuZ) implies ex rr being Surreal st
( rr in R_ SUP & rr <= ll ) )
assume A109: ll in R_ (SuY * SuZ) ; :: thesis: ex rr being Surreal st
( rr in R_ SUP & rr <= ll )
per cases ( ll in comp ((L_ SuY),SuY,SuZ,(R_ SuZ)) or ll in comp ((R_ SuY),SuY,SuZ,(L_ SuZ)) ) by A63, A109, XBOOLE_0:def 3;
suppose ll in comp ((L_ SuY),SuY,SuZ,(R_ SuZ)) ; :: thesis: ex rr being Surreal st
( rr in R_ SUP & rr <= ll )
then consider a1, b1 being Surreal such that
A110: ( ll = ((a1 * SuZ) + (SuY * b1)) - (a1 * b1) & a1 in L_ SuY & b1 in R_ SuZ ) by SURREALR:def 15;
consider Y1 being Element of Y, ey being positive Real such that
A111: ( a1 = (Sum ((r | Y1),((No_omega^ y) | Y1))) + ((uReal . ((r . Y1) - ey)) * ((No_omega^ y) .. Y1)) & Y1 in Y ) by A110;
consider Z1 being Element of Z, ez being positive Real such that
A112: ( b1 = (Sum ((s | Z1),((No_omega^ z) | Z1))) + ((uReal . ((s . Z1) + ez)) * ((No_omega^ z) .. Z1)) & Z1 in Z ) by A110;
set E = ey * ez;
succ Y1 c= (dom r) /\ (dom y) by A5, A2, A111, ORDINAL1:21;
then A113: a1 == (Sum ((r | (succ Y1)),((No_omega^ y) | (succ Y1)))) + ((uReal . (- ey)) * (No_omega^ (y .. Y1))) by A111, Th102;
succ Z1 c= (dom s) /\ (dom z) by A5, A2, A112, ORDINAL1:21;
then A114: b1 == (Sum ((s | (succ Z1)),((No_omega^ z) | (succ Z1)))) + ((uReal . ez) * (No_omega^ (z .. Z1))) by A112, Th102;
consider O1 being Ordinal such that
A115: ( O1 in dom Uyz & Uyz .. O1 == (y .. Y1) + (z .. Z1) ) by A111, A112, A64;
set sO1 = succ O1;
take rr = (Sum (((Sum ((y | Y),(z | Z),Uyz,rY,sZ,S,T)) | O1),((No_omega^ Uyz) | O1))) + ((uReal . (((Sum ((y | Y),(z | Z),Uyz,rY,sZ,S,T)) . O1) + ((ey * ez) / 2))) * ((No_omega^ Uyz) .. O1)); :: thesis: ( rr in R_ SUP & rr <= ll )
thus rr in R_ SUP by A115; :: thesis: rr <= ll
set SS = Sum (((Sum ((y | Y),(z | Z),Uyz,rY,sZ,S,T)) | (succ O1)),((No_omega^ Uyz) | (succ O1)));
set NN = No_omega^ ((y .. Y1) + (z .. Z1));
consider T being Surreal such that
A116: |.T.| infinitely< No_omega^ ((y .. Y1) + (z .. Z1)) and
A117: ((SuY * b1) + (a1 * SuZ)) - (b1 * a1) == ((Sum (((Sum ((y | Y),(z | Z),Uyz,rY,sZ,S,T)) | (succ O1)),((No_omega^ Uyz) | (succ O1)))) + T) - ((uReal . ((- ey) * ez)) * (No_omega^ ((y .. Y1) + (z .. Z1)))) by A111, A112, A113, A114, A115, A14;
A118: - ((uReal . (- (ey * ez))) * (No_omega^ ((y .. Y1) + (z .. Z1)))) == (uReal . (ey * ez)) * (No_omega^ ((y .. Y1) + (z .. Z1))) by Th33;
|.T.| infinitely< (uReal . ((ey * ez) / 2)) * (No_omega^ ((y .. Y1) + (z .. Z1))) by A116, SURREALC:13;
then |.T.| < (uReal . ((ey * ez) / 2)) * (No_omega^ ((y .. Y1) + (z .. Z1))) by SURREALC:9;
then T > - ((uReal . ((ey * ez) / 2)) * (No_omega^ ((y .. Y1) + (z .. Z1)))) by SURREALC:52;
then (Sum (((Sum ((y | Y),(z | Z),Uyz,rY,sZ,S,T)) | (succ O1)),((No_omega^ Uyz) | (succ O1)))) + T > (Sum (((Sum ((y | Y),(z | Z),Uyz,rY,sZ,S,T)) | (succ O1)),((No_omega^ Uyz) | (succ O1)))) - ((uReal . ((ey * ez) / 2)) * (No_omega^ ((y .. Y1) + (z .. Z1)))) by SURREALR:44;
then A119: ((Sum (((Sum ((y | Y),(z | Z),Uyz,rY,sZ,S,T)) | (succ O1)),((No_omega^ Uyz) | (succ O1)))) + T) + (- ((uReal . (- (ey * ez))) * (No_omega^ ((y .. Y1) + (z .. Z1))))) > ((Sum (((Sum ((y | Y),(z | Z),Uyz,rY,sZ,S,T)) | (succ O1)),((No_omega^ Uyz) | (succ O1)))) - ((uReal . ((ey * ez) / 2)) * (No_omega^ ((y .. Y1) + (z .. Z1))))) + ((uReal . (ey * ez)) * (No_omega^ ((y .. Y1) + (z .. Z1)))) by SURREALR:44, A118;
((Sum (((Sum ((y | Y),(z | Z),Uyz,rY,sZ,S,T)) | (succ O1)),((No_omega^ Uyz) | (succ O1)))) + (- ((uReal . ((ey * ez) / 2)) * (No_omega^ ((y .. Y1) + (z .. Z1)))))) + ((uReal . (ey * ez)) * (No_omega^ ((y .. Y1) + (z .. Z1)))) = ((Sum (((Sum ((y | Y),(z | Z),Uyz,rY,sZ,S,T)) | (succ O1)),((No_omega^ Uyz) | (succ O1)))) + ((uReal . (ey * ez)) * (No_omega^ ((y .. Y1) + (z .. Z1))))) - ((uReal . ((ey * ez) / 2)) * (No_omega^ ((y .. Y1) + (z .. Z1)))) by SURREALR:37;
then ((Sum (((Sum ((y | Y),(z | Z),Uyz,rY,sZ,S,T)) | (succ O1)),((No_omega^ Uyz) | (succ O1)))) + (- ((uReal . ((ey * ez) / 2)) * (No_omega^ ((y .. Y1) + (z .. Z1)))))) + ((uReal . (ey * ez)) * (No_omega^ ((y .. Y1) + (z .. Z1)))) == (Sum (((Sum ((y | Y),(z | Z),Uyz,rY,sZ,S,T)) | (succ O1)),((No_omega^ Uyz) | (succ O1)))) + ((uReal . ((ey * ez) - ((ey * ez) / 2))) * (No_omega^ ((y .. Y1) + (z .. Z1)))) by Th30;
then ((Sum (((Sum ((y | Y),(z | Z),Uyz,rY,sZ,S,T)) | (succ O1)),((No_omega^ Uyz) | (succ O1)))) + T) + (- ((uReal . (- (ey * ez))) * (No_omega^ ((y .. Y1) + (z .. Z1))))) > (Sum (((Sum ((y | Y),(z | Z),Uyz,rY,sZ,S,T)) | (succ O1)),((No_omega^ Uyz) | (succ O1)))) + ((uReal . ((ey * ez) / 2)) * (No_omega^ ((y .. Y1) + (z .. Z1)))) by A119, SURREALO:4;
then A120: ll > (Sum (((Sum ((y | Y),(z | Z),Uyz,rY,sZ,S,T)) | (succ O1)),((No_omega^ Uyz) | (succ O1)))) + ((uReal . ((ey * ez) / 2)) * (No_omega^ ((y .. Y1) + (z .. Z1)))) by A110, A117, SURREALO:4;
No_omega^ ((y .. Y1) + (z .. Z1)) == No_omega^ (Uyz .. O1) by A115, SURREALC:24;
then (uReal . ((ey * ez) / 2)) * (No_omega^ ((y .. Y1) + (z .. Z1))) == (uReal . ((ey * ez) / 2)) * (No_omega^ (Uyz .. O1)) by SURREALR:54;
then (Sum (((Sum ((y | Y),(z | Z),Uyz,rY,sZ,S,T)) | (succ O1)),((No_omega^ Uyz) | (succ O1)))) + ((uReal . ((ey * ez) / 2)) * (No_omega^ ((y .. Y1) + (z .. Z1)))) == (Sum (((Sum ((y | Y),(z | Z),Uyz,rY,sZ,S,T)) | (succ O1)),((No_omega^ Uyz) | (succ O1)))) + ((uReal . ((ey * ez) / 2)) * (No_omega^ (Uyz .. O1))) by SURREALR:66;
then A121: ll > (Sum (((Sum ((y | Y),(z | Z),Uyz,rY,sZ,S,T)) | (succ O1)),((No_omega^ Uyz) | (succ O1)))) + ((uReal . ((ey * ez) / 2)) * (No_omega^ (Uyz .. O1))) by A120, SURREALO:4;
succ O1 c= (dom (Sum ((y | Y),(z | Z),Uyz,rY,sZ,S,T))) /\ (dom Uyz) by A60, A115, ORDINAL1:21;
then (Sum (((Sum ((y | Y),(z | Z),Uyz,rY,sZ,S,T)) | (succ O1)),((No_omega^ Uyz) | (succ O1)))) + ((uReal . ((ey * ez) / 2)) * (No_omega^ (Uyz .. O1))) == rr by Th102;
hence rr <= ll by A121, SURREALO:4; :: thesis: verum
end;
suppose ll in comp ((R_ SuY),SuY,SuZ,(L_ SuZ)) ; :: thesis: ex rr being Surreal st
( rr in R_ SUP & rr <= ll )
then consider a1, b1 being Surreal such that
A122: ( ll = ((a1 * SuZ) + (SuY * b1)) - (a1 * b1) & a1 in R_ SuY & b1 in L_ SuZ ) by SURREALR:def 15;
consider Y1 being Element of Y, ey being positive Real such that
A123: ( a1 = (Sum ((r | Y1),((No_omega^ y) | Y1))) + ((uReal . ((r . Y1) + ey)) * ((No_omega^ y) .. Y1)) & Y1 in Y ) by A122;
consider Z1 being Element of Z, ez being positive Real such that
A124: ( b1 = (Sum ((s | Z1),((No_omega^ z) | Z1))) + ((uReal . ((s . Z1) - ez)) * ((No_omega^ z) .. Z1)) & Z1 in Z ) by A122;
set E = ey * ez;
succ Y1 c= (dom r) /\ (dom y) by A5, A2, A123, ORDINAL1:21;
then A125: a1 == (Sum ((r | (succ Y1)),((No_omega^ y) | (succ Y1)))) + ((uReal . ey) * (No_omega^ (y .. Y1))) by A123, Th102;
succ Z1 c= (dom s) /\ (dom z) by A5, A2, A124, ORDINAL1:21;
then A126: b1 == (Sum ((s | (succ Z1)),((No_omega^ z) | (succ Z1)))) + ((uReal . (- ez)) * (No_omega^ (z .. Z1))) by A124, Th102;
consider O1 being Ordinal such that
A127: ( O1 in dom Uyz & Uyz .. O1 == (y .. Y1) + (z .. Z1) ) by A123, A124, A64;
set sO1 = succ O1;
take rr = (Sum (((Sum ((y | Y),(z | Z),Uyz,rY,sZ,S,T)) | O1),((No_omega^ Uyz) | O1))) + ((uReal . (((Sum ((y | Y),(z | Z),Uyz,rY,sZ,S,T)) . O1) + ((ey * ez) / 2))) * ((No_omega^ Uyz) .. O1)); :: thesis: ( rr in R_ SUP & rr <= ll )
thus rr in R_ SUP by A127; :: thesis: rr <= ll
set SS = Sum (((Sum ((y | Y),(z | Z),Uyz,rY,sZ,S,T)) | (succ O1)),((No_omega^ Uyz) | (succ O1)));
set NN = No_omega^ ((y .. Y1) + (z .. Z1));
consider T being Surreal such that
A128: |.T.| infinitely< No_omega^ ((y .. Y1) + (z .. Z1)) and
A129: ((SuY * b1) + (a1 * SuZ)) - (b1 * a1) == ((Sum (((Sum ((y | Y),(z | Z),Uyz,rY,sZ,S,T)) | (succ O1)),((No_omega^ Uyz) | (succ O1)))) + T) - ((uReal . (ey * (- ez))) * (No_omega^ ((y .. Y1) + (z .. Z1)))) by A123, A124, A125, A126, A127, A14;
A130: - ((uReal . (- (ey * ez))) * (No_omega^ ((y .. Y1) + (z .. Z1)))) == (uReal . (ey * ez)) * (No_omega^ ((y .. Y1) + (z .. Z1))) by Th33;
|.T.| infinitely< (uReal . ((ey * ez) / 2)) * (No_omega^ ((y .. Y1) + (z .. Z1))) by A128, SURREALC:13;
then |.T.| < (uReal . ((ey * ez) / 2)) * (No_omega^ ((y .. Y1) + (z .. Z1))) by SURREALC:9;
then T > - ((uReal . ((ey * ez) / 2)) * (No_omega^ ((y .. Y1) + (z .. Z1)))) by SURREALC:52;
then (Sum (((Sum ((y | Y),(z | Z),Uyz,rY,sZ,S,T)) | (succ O1)),((No_omega^ Uyz) | (succ O1)))) + T > (Sum (((Sum ((y | Y),(z | Z),Uyz,rY,sZ,S,T)) | (succ O1)),((No_omega^ Uyz) | (succ O1)))) - ((uReal . ((ey * ez) / 2)) * (No_omega^ ((y .. Y1) + (z .. Z1)))) by SURREALR:44;
then A131: ((Sum (((Sum ((y | Y),(z | Z),Uyz,rY,sZ,S,T)) | (succ O1)),((No_omega^ Uyz) | (succ O1)))) + T) + (- ((uReal . (- (ey * ez))) * (No_omega^ ((y .. Y1) + (z .. Z1))))) > ((Sum (((Sum ((y | Y),(z | Z),Uyz,rY,sZ,S,T)) | (succ O1)),((No_omega^ Uyz) | (succ O1)))) - ((uReal . ((ey * ez) / 2)) * (No_omega^ ((y .. Y1) + (z .. Z1))))) + ((uReal . (ey * ez)) * (No_omega^ ((y .. Y1) + (z .. Z1)))) by SURREALR:44, A130;
((Sum (((Sum ((y | Y),(z | Z),Uyz,rY,sZ,S,T)) | (succ O1)),((No_omega^ Uyz) | (succ O1)))) + (- ((uReal . ((ey * ez) / 2)) * (No_omega^ ((y .. Y1) + (z .. Z1)))))) + ((uReal . (ey * ez)) * (No_omega^ ((y .. Y1) + (z .. Z1)))) = ((Sum (((Sum ((y | Y),(z | Z),Uyz,rY,sZ,S,T)) | (succ O1)),((No_omega^ Uyz) | (succ O1)))) + ((uReal . (ey * ez)) * (No_omega^ ((y .. Y1) + (z .. Z1))))) - ((uReal . ((ey * ez) / 2)) * (No_omega^ ((y .. Y1) + (z .. Z1)))) by SURREALR:37;
then ((Sum (((Sum ((y | Y),(z | Z),Uyz,rY,sZ,S,T)) | (succ O1)),((No_omega^ Uyz) | (succ O1)))) + (- ((uReal . ((ey * ez) / 2)) * (No_omega^ ((y .. Y1) + (z .. Z1)))))) + ((uReal . (ey * ez)) * (No_omega^ ((y .. Y1) + (z .. Z1)))) == (Sum (((Sum ((y | Y),(z | Z),Uyz,rY,sZ,S,T)) | (succ O1)),((No_omega^ Uyz) | (succ O1)))) + ((uReal . ((ey * ez) - ((ey * ez) / 2))) * (No_omega^ ((y .. Y1) + (z .. Z1)))) by Th30;
then ((Sum (((Sum ((y | Y),(z | Z),Uyz,rY,sZ,S,T)) | (succ O1)),((No_omega^ Uyz) | (succ O1)))) + T) + (- ((uReal . (- (ey * ez))) * (No_omega^ ((y .. Y1) + (z .. Z1))))) > (Sum (((Sum ((y | Y),(z | Z),Uyz,rY,sZ,S,T)) | (succ O1)),((No_omega^ Uyz) | (succ O1)))) + ((uReal . ((ey * ez) / 2)) * (No_omega^ ((y .. Y1) + (z .. Z1)))) by A131, SURREALO:4;
then A132: ll > (Sum (((Sum ((y | Y),(z | Z),Uyz,rY,sZ,S,T)) | (succ O1)),((No_omega^ Uyz) | (succ O1)))) + ((uReal . ((ey * ez) / 2)) * (No_omega^ ((y .. Y1) + (z .. Z1)))) by A122, A129, SURREALO:4;
No_omega^ ((y .. Y1) + (z .. Z1)) == No_omega^ (Uyz .. O1) by A127, SURREALC:24;
then (uReal . ((ey * ez) / 2)) * (No_omega^ ((y .. Y1) + (z .. Z1))) == (uReal . ((ey * ez) / 2)) * (No_omega^ (Uyz .. O1)) by SURREALR:54;
then (Sum (((Sum ((y | Y),(z | Z),Uyz,rY,sZ,S,T)) | (succ O1)),((No_omega^ Uyz) | (succ O1)))) + ((uReal . ((ey * ez) / 2)) * (No_omega^ ((y .. Y1) + (z .. Z1)))) == (Sum (((Sum ((y | Y),(z | Z),Uyz,rY,sZ,S,T)) | (succ O1)),((No_omega^ Uyz) | (succ O1)))) + ((uReal . ((ey * ez) / 2)) * (No_omega^ (Uyz .. O1))) by SURREALR:66;
then A133: ll > (Sum (((Sum ((y | Y),(z | Z),Uyz,rY,sZ,S,T)) | (succ O1)),((No_omega^ Uyz) | (succ O1)))) + ((uReal . ((ey * ez) / 2)) * (No_omega^ (Uyz .. O1))) by A132, SURREALO:4;
succ O1 c= (dom (Sum ((y | Y),(z | Z),Uyz,rY,sZ,S,T))) /\ (dom Uyz) by A60, A127, ORDINAL1:21;
then (Sum (((Sum ((y | Y),(z | Z),Uyz,rY,sZ,S,T)) | (succ O1)),((No_omega^ Uyz) | (succ O1)))) + ((uReal . ((ey * ez) / 2)) * (No_omega^ (Uyz .. O1))) == rr by Th102;
hence rr <= ll by A133, SURREALO:4; :: thesis: verum
end;
end;
end;
A134: for ll being Surreal st ll in L_ SUP holds
ex rr being Surreal st
( rr in L_ (SuY * SuZ) & ll <= rr )
proof
let ll be Surreal; :: thesis: ( ll in L_ SUP implies ex rr being Surreal st
( rr in L_ (SuY * SuZ) & ll <= rr ) )
assume A135: ll in L_ SUP ; :: thesis: ex rr being Surreal st
( rr in L_ (SuY * SuZ) & ll <= rr )
consider O1 being Element of dom Uyz, e being positive Real such that
A136: ( ll = (Sum (((Sum ((y | Y),(z | Z),Uyz,rY,sZ,S,T)) | O1),((No_omega^ Uyz) | O1))) + ((uReal . (((Sum ((y | Y),(z | Z),Uyz,rY,sZ,S,T)) . O1) - e)) * ((No_omega^ Uyz) .. O1)) & O1 in dom Uyz ) by A135;
consider Y1, Z1 being Ordinal such that
A137: Y1 in Y and
A138: Z1 in Z and
A139: Uyz .. O1 == (y .. Y1) + (z .. Z1) by A90, A136;
set ey = e;
set ez = 1 / 2;
set E = e * (1 / 2);
set a1 = (Sum ((r | Y1),((No_omega^ y) | Y1))) + ((uReal . ((r . Y1) - e)) * ((No_omega^ y) .. Y1));
set b1 = (Sum ((s | Z1),((No_omega^ z) | Z1))) + ((uReal . ((s . Z1) - (1 / 2))) * ((No_omega^ z) .. Z1));
succ Y1 c= (dom r) /\ (dom y) by A5, A2, A137, ORDINAL1:21;
then A140: (Sum ((r | Y1),((No_omega^ y) | Y1))) + ((uReal . ((r . Y1) - e)) * ((No_omega^ y) .. Y1)) == (Sum ((r | (succ Y1)),((No_omega^ y) | (succ Y1)))) + ((uReal . (- e)) * (No_omega^ (y .. Y1))) by Th102;
succ Z1 c= (dom s) /\ (dom z) by A5, A2, A138, ORDINAL1:21;
then A141: (Sum ((s | Z1),((No_omega^ z) | Z1))) + ((uReal . ((s . Z1) - (1 / 2))) * ((No_omega^ z) .. Z1)) == (Sum ((s | (succ Z1)),((No_omega^ z) | (succ Z1)))) + ((uReal . (- (1 / 2))) * (No_omega^ (z .. Z1))) by Th102;
take rr = ((SuY * ((Sum ((s | Z1),((No_omega^ z) | Z1))) + ((uReal . ((s . Z1) - (1 / 2))) * ((No_omega^ z) .. Z1)))) + (((Sum ((r | Y1),((No_omega^ y) | Y1))) + ((uReal . ((r . Y1) - e)) * ((No_omega^ y) .. Y1))) * SuZ)) - (((Sum ((s | Z1),((No_omega^ z) | Z1))) + ((uReal . ((s . Z1) - (1 / 2))) * ((No_omega^ z) .. Z1))) * ((Sum ((r | Y1),((No_omega^ y) | Y1))) + ((uReal . ((r . Y1) - e)) * ((No_omega^ y) .. Y1)))); :: thesis: ( rr in L_ (SuY * SuZ) & ll <= rr )
set sO1 = succ O1;
set SS = Sum (((Sum ((y | Y),(z | Z),Uyz,rY,sZ,S,T)) | (succ O1)),((No_omega^ Uyz) | (succ O1)));
set NN = No_omega^ ((y .. Y1) + (z .. Z1));
consider T being Surreal such that
A142: |.T.| infinitely< No_omega^ ((y .. Y1) + (z .. Z1)) and
A143: rr == ((Sum (((Sum ((y | Y),(z | Z),Uyz,rY,sZ,S,T)) | (succ O1)),((No_omega^ Uyz) | (succ O1)))) + T) - ((uReal . ((- e) * (- (1 / 2)))) * (No_omega^ ((y .. Y1) + (z .. Z1)))) by A136, A137, A138, A140, A141, A139, A14;
succ O1 c= (dom (Sum ((y | Y),(z | Z),Uyz,rY,sZ,S,T))) /\ (dom Uyz) by A60, A136, ORDINAL1:21;
then A144: (Sum (((Sum ((y | Y),(z | Z),Uyz,rY,sZ,S,T)) | (succ O1)),((No_omega^ Uyz) | (succ O1)))) + ((uReal . (- e)) * (No_omega^ (Uyz .. O1))) == ll by Th102, A136;
( (Sum ((s | Z1),((No_omega^ z) | Z1))) + ((uReal . ((s . Z1) - (1 / 2))) * ((No_omega^ z) .. Z1)) in L_ SuZ & (Sum ((r | Y1),((No_omega^ y) | Y1))) + ((uReal . ((r . Y1) - e)) * ((No_omega^ y) .. Y1)) in L_ SuY ) by A137, A138;
then rr in comp ((L_ SuY),SuY,SuZ,(L_ SuZ)) by SURREALR:def 15;
hence rr in L_ (SuY * SuZ) by A63, XBOOLE_0:def 3; :: thesis: ll <= rr
A145: - ((uReal . (- (- (e * (1 / 2))))) * (No_omega^ ((y .. Y1) + (z .. Z1)))) == (uReal . (- (e * (1 / 2)))) * (No_omega^ ((y .. Y1) + (z .. Z1))) by Th33;
|.T.| infinitely< (uReal . (e / 2)) * (No_omega^ ((y .. Y1) + (z .. Z1))) by A142, SURREALC:13;
then |.T.| < (uReal . (e / 2)) * (No_omega^ ((y .. Y1) + (z .. Z1))) by SURREALC:9;
then T > - ((uReal . (e / 2)) * (No_omega^ ((y .. Y1) + (z .. Z1)))) by SURREALC:52;
then (Sum (((Sum ((y | Y),(z | Z),Uyz,rY,sZ,S,T)) | (succ O1)),((No_omega^ Uyz) | (succ O1)))) + T > (Sum (((Sum ((y | Y),(z | Z),Uyz,rY,sZ,S,T)) | (succ O1)),((No_omega^ Uyz) | (succ O1)))) + (- ((uReal . (e / 2)) * (No_omega^ ((y .. Y1) + (z .. Z1))))) by SURREALR:44;
then A146: ((Sum (((Sum ((y | Y),(z | Z),Uyz,rY,sZ,S,T)) | (succ O1)),((No_omega^ Uyz) | (succ O1)))) + T) + (- ((uReal . (e * (1 / 2))) * (No_omega^ ((y .. Y1) + (z .. Z1))))) > ((Sum (((Sum ((y | Y),(z | Z),Uyz,rY,sZ,S,T)) | (succ O1)),((No_omega^ Uyz) | (succ O1)))) - ((uReal . (e / 2)) * (No_omega^ ((y .. Y1) + (z .. Z1))))) + ((uReal . (- (e * (1 / 2)))) * (No_omega^ ((y .. Y1) + (z .. Z1)))) by SURREALR:44, A145;
((Sum (((Sum ((y | Y),(z | Z),Uyz,rY,sZ,S,T)) | (succ O1)),((No_omega^ Uyz) | (succ O1)))) + (- ((uReal . (e / 2)) * (No_omega^ ((y .. Y1) + (z .. Z1)))))) + ((uReal . (- (e * (1 / 2)))) * (No_omega^ ((y .. Y1) + (z .. Z1)))) = ((Sum (((Sum ((y | Y),(z | Z),Uyz,rY,sZ,S,T)) | (succ O1)),((No_omega^ Uyz) | (succ O1)))) + ((uReal . (- (e * (1 / 2)))) * (No_omega^ ((y .. Y1) + (z .. Z1))))) - ((uReal . (e / 2)) * (No_omega^ ((y .. Y1) + (z .. Z1)))) by SURREALR:37;
then ((Sum (((Sum ((y | Y),(z | Z),Uyz,rY,sZ,S,T)) | (succ O1)),((No_omega^ Uyz) | (succ O1)))) + (- ((uReal . (e / 2)) * (No_omega^ ((y .. Y1) + (z .. Z1)))))) + ((uReal . (- (e * (1 / 2)))) * (No_omega^ ((y .. Y1) + (z .. Z1)))) == (Sum (((Sum ((y | Y),(z | Z),Uyz,rY,sZ,S,T)) | (succ O1)),((No_omega^ Uyz) | (succ O1)))) + ((uReal . ((- (e * (1 / 2))) - (e / 2))) * (No_omega^ ((y .. Y1) + (z .. Z1)))) by Th30;
then ((Sum (((Sum ((y | Y),(z | Z),Uyz,rY,sZ,S,T)) | (succ O1)),((No_omega^ Uyz) | (succ O1)))) + T) + (- ((uReal . (e * (1 / 2))) * (No_omega^ ((y .. Y1) + (z .. Z1))))) > (Sum (((Sum ((y | Y),(z | Z),Uyz,rY,sZ,S,T)) | (succ O1)),((No_omega^ Uyz) | (succ O1)))) + ((uReal . (- e)) * (No_omega^ ((y .. Y1) + (z .. Z1)))) by A146, SURREALO:4;
then A147: rr > (Sum (((Sum ((y | Y),(z | Z),Uyz,rY,sZ,S,T)) | (succ O1)),((No_omega^ Uyz) | (succ O1)))) + ((uReal . (- e)) * (No_omega^ ((y .. Y1) + (z .. Z1)))) by A143, SURREALO:4;
No_omega^ ((y .. Y1) + (z .. Z1)) == No_omega^ (Uyz .. O1) by A139, SURREALC:24;
then (uReal . (- e)) * (No_omega^ ((y .. Y1) + (z .. Z1))) == (uReal . (- e)) * (No_omega^ (Uyz .. O1)) by SURREALR:54;
then (Sum (((Sum ((y | Y),(z | Z),Uyz,rY,sZ,S,T)) | (succ O1)),((No_omega^ Uyz) | (succ O1)))) + ((uReal . (- e)) * (No_omega^ ((y .. Y1) + (z .. Z1)))) == (Sum (((Sum ((y | Y),(z | Z),Uyz,rY,sZ,S,T)) | (succ O1)),((No_omega^ Uyz) | (succ O1)))) + ((uReal . (- e)) * (No_omega^ (Uyz .. O1))) by SURREALR:66;
then rr > (Sum (((Sum ((y | Y),(z | Z),Uyz,rY,sZ,S,T)) | (succ O1)),((No_omega^ Uyz) | (succ O1)))) + ((uReal . (- e)) * (No_omega^ (Uyz .. O1))) by A147, SURREALO:4;
then rr > ll by A144, SURREALO:4;
hence rr >= ll by SURREALO:6; :: thesis: verum
end;
( SUP = [(L_ SUP),(R_ SUP)] & SuY * SuZ = [(L_ (SuY * SuZ)),(R_ (SuY * SuZ))] ) ;
then SuY * SuZ == SUP by A68, A96, A108, A134, SURREAL0:44;
then A148: SuY * SuZ == Sum ((Sum ((y | Y),(z | Z),yz,rY,sZ,S,T)),(No_omega^ yz)) by A60, A13, A62, SURREALO:4;
(Sum ((r | Y),((No_omega^ y) | Y))) * (Sum ((s | Z),((No_omega^ z) | Z))) == SuY * SuZ by Th29, A10, A11;
hence (Sum ((r | Y),((No_omega^ y) | Y))) * (Sum ((s | Z),((No_omega^ z) | Z))) == Sum ((Sum ((y | Y),(z | Z),yz,(r | Y),(s | Z),S,T)),(No_omega^ yz)) by A148, SURREALO:4; :: thesis: verum
end;
suppose not Y is limit_ordinal ; :: thesis: (Sum ((r | Y),((No_omega^ y) | Y))) * (Sum ((s | Z),((No_omega^ z) | Z))) == Sum ((Sum ((y | Y),(z | Z),yz,(r | Y),(s | Z),S,T)),(No_omega^ yz))
then consider Y1 being Ordinal such that
A149: Y = succ Y1 by ORDINAL1:29;
A150: ( No_omega^ (z | Z) = (No_omega^ z) | Z & (No_omega^ y) | Y = No_omega^ (y | Y) & (No_omega^ y) | Y1 = No_omega^ (y | Y1) ) by SURREALC:88;
Y1 c= Y by A149, ORDINAL3:1;
then A156: Y1 c= dom y by A5;
A152: ( rY | Y1 = r | Y1 & (y | Y) | Y1 = y | Y1 ) by A149, ORDINAL3:1, RELAT_1:74;
A153: Y c= (dom r) /\ (dom y) by A5, A2;
A154: Y c= S by A1, A5;
A155: dom (z | Z) c= T by A5, A6, A1;
A157: Y1 in dom y by A5, A149, ORDINAL1:6;
then A158: y . Y1 = y .. Y1 by Def5;
A159: ( rY /^ Y1 = <%(r . Y1)%> & (y | Y) /^ Y1 = <%(y .. Y1)%> ) by A158, A5, A149, A2, Th9;
y . Y1 in rng y by A157, FUNCT_1:def 3;
then A160: {(y .. Y1)} c= rng y by A158, ZFMISC_1:31;
{(y .. Y1)} ++ (rng (z | Z)) c= (rng y) ++ (rng z) by A160, Th34;
then Unique_No ({(y .. Y1)} ++ (rng (z | Z))) c= Unique_No ((rng y) ++ (rng z)) by Th48;
then A161: Unique_No ({(y .. Y1)} ++ (rng (z | Z))) c= rng yz by A1;
Y1 (+) Z in O by A5, A149, ORDINAL1:6, ORDINAL7:94;
then A162: (Sum ((r | Y1),((No_omega^ y) | Y1))) * (Sum (sZ,((No_omega^ z) | Z))) == Sum ((Sum ((y | Y1),(z | Z),yz,(r | Y1),sZ,S,T)),(No_omega^ yz)) by A4, A5, A156;
A163: Sum ((Sum (<%(y .. Y1)%>,(z | Z),yz,<%(r . Y1)%>,sZ,S,T)),(No_omega^ yz)) == ((uReal . (r . Y1)) * (No_omega^ (y .. Y1))) * (Sum (sZ,(No_omega^ (z | Z)))) by A161, A6, A155, Th95;
( (Sum ((Sum (((y | Y) | Y1),(z | Z),yz,(rY | Y1),sZ,S,T)),(No_omega^ yz))) + (Sum ((Sum (((y | Y) /^ Y1),(z | Z),yz,(rY /^ Y1),sZ,S,T)),(No_omega^ yz))) == ((Sum ((r | Y1),((No_omega^ y) | Y1))) * (Sum (sZ,((No_omega^ z) | Z)))) + (((uReal . (r . Y1)) * (No_omega^ (y .. Y1))) * (Sum (sZ,((No_omega^ z) | Z)))) & ((Sum ((r | Y1),((No_omega^ y) | Y1))) * (Sum (sZ,((No_omega^ z) | Z)))) + (((uReal . (r . Y1)) * (No_omega^ (y .. Y1))) * (Sum (sZ,((No_omega^ z) | Z)))) == ((Sum ((r | Y1),((No_omega^ y) | Y1))) + ((uReal . (r . Y1)) * (No_omega^ (y .. Y1)))) * (Sum (sZ,((No_omega^ z) | Z))) ) by A162, A163, A152, A159, A150, SURREALR:66, SURREALR:67;
then ( (Sum ((Sum (((y | Y) | Y1),(z | Z),yz,(rY | Y1),sZ,S,T)),(No_omega^ yz))) + (Sum ((Sum (((y | Y) /^ Y1),(z | Z),yz,(rY /^ Y1),sZ,S,T)),(No_omega^ yz))) == ((Sum ((r | Y1),((No_omega^ y) | Y1))) + ((uReal . (r . Y1)) * (No_omega^ (y .. Y1)))) * (Sum (sZ,((No_omega^ z) | Z))) & ((Sum ((r | Y1),((No_omega^ y) | Y1))) + ((uReal . (r . Y1)) * (No_omega^ (y .. Y1)))) * (Sum (sZ,((No_omega^ z) | Z))) == (Sum ((r | Y),((No_omega^ y) | Y))) * (Sum (sZ,((No_omega^ z) | Z))) ) by SURREALO:4, SURREALR:54, A153, A150, A149, Th64;
then A164: (Sum ((Sum (((y | Y) | Y1),(z | Z),yz,(rY | Y1),sZ,S,T)),(No_omega^ yz))) + (Sum ((Sum (((y | Y) /^ Y1),(z | Z),yz,(rY /^ Y1),sZ,S,T)),(No_omega^ yz))) == (Sum ((r | Y),((No_omega^ y) | Y))) * (Sum (sZ,((No_omega^ z) | Z))) by SURREALO:4;
Sum ((Sum ((y | Y),(z | Z),yz,rY,(s | Z),S,T)),(No_omega^ yz)) == (Sum ((Sum (((y | Y) | Y1),(z | Z),yz,(rY | Y1),sZ,S,T)),(No_omega^ yz))) + (Sum ((Sum (((y | Y) /^ Y1),(z | Z),yz,(rY /^ Y1),sZ,S,T)),(No_omega^ yz))) by A149, ORDINAL3:1, A154, A155, A6, Th99;
hence (Sum ((r | Y),((No_omega^ y) | Y))) * (Sum ((s | Z),((No_omega^ z) | Z))) == Sum ((Sum ((y | Y),(z | Z),yz,(r | Y),(s | Z),S,T)),(No_omega^ yz)) by A164, SURREALO:4; :: thesis: verum
end;
suppose not Z is limit_ordinal ; :: thesis: (Sum ((r | Y),((No_omega^ y) | Y))) * (Sum ((s | Z),((No_omega^ z) | Z))) == Sum ((Sum ((y | Y),(z | Z),yz,(r | Y),(s | Z),S,T)),(No_omega^ yz))
then consider Z1 being Ordinal such that
A165: Z = succ Z1 by ORDINAL1:29;
A166: ( No_omega^ (z | Z) = (No_omega^ z) | Z & (No_omega^ y) | Y = No_omega^ (y | Y) & (No_omega^ z) | Z1 = No_omega^ (z | Z1) ) by SURREALC:88;
A167: Z1 c= Z by A165, ORDINAL3:1;
A168: ( sZ | Z1 = s | Z1 & (z | Z) | Z1 = z | Z1 ) by A165, ORDINAL3:1, RELAT_1:74;
A169: Z c= (dom s) /\ (dom z) by A5, A2;
A170: Z c= T by A1, A5;
A171: dom (y | Y) c= S by A6, A5, A1;
A172: Z1 c= dom z by A167, A5;
A173: Z1 in dom z by A5, A165, ORDINAL1:6;
then A174: z . Z1 = z .. Z1 by Def5;
A175: ( sZ /^ Z1 = <%(s . Z1)%> & (z | Z) /^ Z1 = <%(z .. Z1)%> ) by A174, A5, A165, A2, Th9;
z . Z1 in rng z by A173, FUNCT_1:def 3;
then A176: {(z .. Z1)} c= rng z by A174, ZFMISC_1:31;
{(z .. Z1)} ++ (rng (y | Y)) c= (rng y) ++ (rng z) by A176, Th34;
then Unique_No ({(z .. Z1)} ++ (rng (y | Y))) c= Unique_No ((rng y) ++ (rng z)) by Th48;
then A177: Unique_No ({(z .. Z1)} ++ (rng (y | Y))) c= rng yz by A1;
Y (+) Z1 in O by A5, A165, ORDINAL1:6, ORDINAL7:94;
then A178: (Sum (rY,((No_omega^ y) | Y))) * (Sum ((s | Z1),((No_omega^ z) | Z1))) == Sum ((Sum ((y | Y),(z | Z1),yz,rY,(s | Z1),S,T)),(No_omega^ yz)) by A4, A5, A172;
A179: Sum ((Sum ((y | Y),<%(z .. Z1)%>,yz,rY,<%(s . Z1)%>,S,T)),(No_omega^ yz)) == ((uReal . (s . Z1)) * (No_omega^ (z .. Z1))) * (Sum (rY,(No_omega^ (y | Y)))) by A177, A6, A171, Th96;
( (Sum ((Sum ((y | Y),(z | Z1),yz,rY,(s | Z1),S,T)),(No_omega^ yz))) + (Sum ((Sum ((y | Y),((z | Z) /^ Z1),yz,rY,(sZ /^ Z1),S,T)),(No_omega^ yz))) == ((Sum (rY,((No_omega^ y) | Y))) * (Sum ((s | Z1),((No_omega^ z) | Z1)))) + (((uReal . (s . Z1)) * (No_omega^ (z .. Z1))) * (Sum (rY,(No_omega^ (y | Y))))) & ((Sum (rY,((No_omega^ y) | Y))) * (Sum ((s | Z1),((No_omega^ z) | Z1)))) + (((uReal . (s . Z1)) * (No_omega^ (z .. Z1))) * (Sum (rY,(No_omega^ (y | Y))))) == ((Sum ((s | Z1),((No_omega^ z) | Z1))) + ((uReal . (s . Z1)) * (No_omega^ (z .. Z1)))) * (Sum (rY,((No_omega^ y) | Y))) ) by A178, A179, A175, A166, SURREALR:66, SURREALR:67;
then ( (Sum ((Sum ((y | Y),(z | Z1),yz,rY,(s | Z1),S,T)),(No_omega^ yz))) + (Sum ((Sum ((y | Y),((z | Z) /^ Z1),yz,rY,(sZ /^ Z1),S,T)),(No_omega^ yz))) == ((Sum ((s | Z1),((No_omega^ z) | Z1))) + ((uReal . (s . Z1)) * (No_omega^ (z .. Z1)))) * (Sum (rY,((No_omega^ y) | Y))) & ((Sum ((s | Z1),((No_omega^ z) | Z1))) + ((uReal . (s . Z1)) * (No_omega^ (z .. Z1)))) * (Sum (rY,((No_omega^ y) | Y))) == (Sum ((r | Y),((No_omega^ y) | Y))) * (Sum (sZ,((No_omega^ z) | Z))) ) by SURREALO:4, SURREALR:54, A169, A166, A165, Th64;
then A180: (Sum ((Sum ((y | Y),((z | Z) | Z1),yz,rY,(sZ | Z1),S,T)),(No_omega^ yz))) + (Sum ((Sum ((y | Y),((z | Z) /^ Z1),yz,rY,(sZ /^ Z1),S,T)),(No_omega^ yz))) == (Sum ((r | Y),((No_omega^ y) | Y))) * (Sum (sZ,((No_omega^ z) | Z))) by A168, SURREALO:4;
Sum ((Sum ((y | Y),(z | Z),yz,rY,(s | Z),S,T)),(No_omega^ yz)) == (Sum ((Sum ((y | Y),((z | Z) | Z1),yz,rY,(sZ | Z1),S,T)),(No_omega^ yz))) + (Sum ((Sum ((y | Y),((z | Z) /^ Z1),yz,rY,(sZ /^ Z1),S,T)),(No_omega^ yz))) by A165, ORDINAL3:1, A170, A171, A6, Th100;
hence (Sum ((r | Y),((No_omega^ y) | Y))) * (Sum ((s | Z),((No_omega^ z) | Z))) == Sum ((Sum ((y | Y),(z | Z),yz,(r | Y),(s | Z),S,T)),(No_omega^ yz)) by A180, SURREALO:4; :: thesis: verum
end;
end;
end;
A181: ( dom (No_omega^ y) = dom y & dom (No_omega^ z) = dom z ) by SURREALC:def 22;
for A being Ordinal holds S1[A] from ORDINAL1:sch 2(A3);
 then S1[(dom y) (+) (dom z)] ;
then (Sum ((r | (dom y)),((No_omega^ y) | (dom y)))) * (Sum ((s | (dom z)),((No_omega^ z) | (dom z)))) == Sum ((Sum ((y | (dom y)),(z | (dom z)),yz,(r | (dom y)),(s | (dom z)),S,T)),(No_omega^ yz)) ;
hence (Sum (r,(No_omega^ y))) * (Sum (s,(No_omega^ z))) == Sum ((Sum (y,z,yz,r,s,S,T)),(No_omega^ yz)) by A181, A2; :: thesis: verum