set s = Partial_Sums (r,y);
(dom y) /\ (dom r) in succ (dom y) by XBOOLE_1:17, ORDINAL1:22;
then A1: ( dom (Partial_Sums (r,y)) = succ ((dom y) /\ (dom r)) & succ ((dom y) /\ (dom r)) c= succ (dom y) ) by ORDINAL1:21, Def17;
Partial_Sums (r,y),y,r simplest_up_to dom (Partial_Sums (r,y)) by Def17;
then (Partial_Sums (r,y)) | (dom (Partial_Sums (r,y))) is one-to-one by A1, Th96;
hence Partial_Sums (r,y) is one-to-one ; :: thesis: verum