let x be Surreal; :: thesis: for r being non-zero Sequence of REAL
for y being strictly_decreasing Surreal-Sequence
for alpha being Ordinal st r,y,alpha name_like x holds
r | alpha,y | alpha,alpha name_like x
let r be non-zero Sequence of REAL ; :: thesis: for y being strictly_decreasing Surreal-Sequence
for alpha being Ordinal st r,y,alpha name_like x holds
r | alpha,y | alpha,alpha name_like x
let y be strictly_decreasing Surreal-Sequence; :: thesis: for alpha being Ordinal st r,y,alpha name_like x holds
r | alpha,y | alpha,alpha name_like x
let A be Ordinal; :: thesis: ( r,y,A name_like x implies r | A,y | A,A name_like x )
assume A1: r,y,A name_like x ; :: thesis: r | A,y | A,A name_like x
A2: ( dom (r | A) = A & dom (y | A) = A ) by A1, RELAT_1:62;
thus ( A c= dom (r | A) & dom (r | A) = dom (y | A) ) by A2; :: according to SURREALC:def 19 :: thesis: for beta being Ordinal st beta in A holds
for Pb being Surreal st Pb = (Partial_Sums ((r | A),(y | A))) . beta holds
( not x == Pb & (r | A) . beta = omega-r (x - Pb) & (y | A) . beta = omega-y (x - Pb) )
let B be Ordinal; :: thesis: ( B in A implies for Pb being Surreal st Pb = (Partial_Sums ((r | A),(y | A))) . B holds
( not x == Pb & (r | A) . B = omega-r (x - Pb) & (y | A) . B = omega-y (x - Pb) ) )
assume A3: B in A ; :: thesis: for Pb being Surreal st Pb = (Partial_Sums ((r | A),(y | A))) . B holds
( not x == Pb & (r | A) . B = omega-r (x - Pb) & (y | A) . B = omega-y (x - Pb) )
let Pb be Surreal; :: thesis: ( Pb = (Partial_Sums ((r | A),(y | A))) . B implies ( not x == Pb & (r | A) . B = omega-r (x - Pb) & (y | A) . B = omega-y (x - Pb) ) )
assume A4: Pb = (Partial_Sums ((r | A),(y | A))) . B ; :: thesis: ( not x == Pb & (r | A) . B = omega-r (x - Pb) & (y | A) . B = omega-y (x - Pb) )
A5: Partial_Sums ((r | A),(y | A)) = (Partial_Sums (r,y)) | (succ A) by Th85;
B in succ A by A3, ORDINAL1:8;
then Pb = (Partial_Sums (r,y)) . B by A4, A5, FUNCT_1:49;
then ( not x == Pb & r . B = omega-r (x - Pb) & y . B = omega-y (x - Pb) ) by A1, A3;
hence ( not x == Pb & (r | A) . B = omega-r (x - Pb) & (y | A) . B = omega-y (x - Pb) ) by A3, FUNCT_1:49; :: thesis: verum