let x be Surreal; :: thesis: for r being Sequence of REAL
for y, s1, s2 being Sequence
for alpha being Ordinal st s1 | alpha = s2 | alpha & x in_meets_terms s1,y,r,alpha holds
x in_meets_terms s2,y,r,alpha
let r be Sequence of REAL ; :: thesis: for y, s1, s2 being Sequence
for alpha being Ordinal st s1 | alpha = s2 | alpha & x in_meets_terms s1,y,r,alpha holds
x in_meets_terms s2,y,r,alpha
let y, s1, s2 be Sequence; :: thesis: for alpha being Ordinal st s1 | alpha = s2 | alpha & x in_meets_terms s1,y,r,alpha holds
x in_meets_terms s2,y,r,alpha
let alpha be Ordinal; :: thesis: ( s1 | alpha = s2 | alpha & x in_meets_terms s1,y,r,alpha implies x in_meets_terms s2,y,r,alpha )
assume that
A1: s1 | alpha = s2 | alpha and
A2: x in_meets_terms s1,y,r,alpha ; :: thesis: x in_meets_terms s2,y,r,alpha
let beta be Ordinal; :: according to SURREALC:def 14 :: thesis: for sb, yb being Surreal st beta in alpha & sb = s2 . beta & yb = y . beta holds
x is sb,yb,r . beta _term
let sb, yb be Surreal; :: thesis: ( beta in alpha & sb = s2 . beta & yb = y . beta implies x is sb,yb,r . beta _term )
assume A3: ( beta in alpha & sb = s2 . beta & yb = y . beta ) ; :: thesis: x is sb,yb,r . beta _term
( s2 . beta = (s2 | alpha) . beta & s1 . beta = (s1 | alpha) . beta ) by A3, FUNCT_1:49;
hence x is sb,yb,r . beta _term by A3, A2, A1; :: thesis: verum