consider y being strictly_decreasing uSurreal-Sequence such that
A1: ( dom y = dom (name-r x) & Sum ((name-r x),y) == x ) by Def22;
take y ; :: thesis: ( dom (name-r x) = dom y & Sum ((name-r x),y) == x )
thus ( dom (name-r x) = dom y & Sum ((name-r x),y) == x ) by A1; :: thesis: verum