set s = Partial_Sums (r,y);
dom (Partial_Sums (r,y)) = dom (born (Partial_Sums (r,y))) by Def20;
then A1: (born (Partial_Sums (r,y))) | (dom (Partial_Sums (r,y))) = born (Partial_Sums (r,y)) ;
( Partial_Sums (r,y),y,r simplest_up_to dom (Partial_Sums (r,y)) & (Partial_Sums (r,y)) | (dom (Partial_Sums (r,y))) is one-to-one ) by Def17;
hence born (Partial_Sums (r,y)) is increasing by A1, Th97; :: thesis: verum