let P1, P2 be uSurreal-Sequence; :: thesis: ( dom P1 = succ ((dom r) /\ (dom y)) & ( for A being Ordinal st A in dom P1 holds
P1,y,r simplest_on_position A ) & dom P2 = succ ((dom r) /\ (dom y)) & ( for A being Ordinal st A in dom P2 holds
P2,y,r simplest_on_position A ) implies P1 = P2 )
assume that
A2: ( dom P1 = succ ((dom r) /\ (dom y)) & ( for A being Ordinal st A in dom P1 holds
P1,y,r simplest_on_position A ) ) and
A3: ( dom P2 = succ ((dom r) /\ (dom y)) & ( for A being Ordinal st A in dom P2 holds
P2,y,r simplest_on_position A ) ) ; :: thesis: P1 = P2
( P1,y,r simplest_up_to dom P1 & P2,y,r simplest_up_to dom P2 ) by A2, A3;
then P1 | (dom P1) = P2 | (dom P2) by A2, A3, Th77;
hence P1 = P2 ; :: thesis: verum