consider s being uSurreal-Sequence such that
A1: ( dom s = succ ((dom r) /\ (dom y)) & s,y,r simplest_up_to dom s ) by Th82;
take s ; :: thesis: ( dom s = succ ((dom r) /\ (dom y)) & ( for A being Ordinal st A in dom s holds
s,y,r simplest_on_position A ) )
thus dom s = succ ((dom r) /\ (dom y)) by A1; :: thesis: for A being Ordinal st A in dom s holds
s,y,r simplest_on_position A
thus for A being Ordinal st A in dom s holds
s,y,r simplest_on_position A by A1; :: thesis: verum