A1: dom (Partial_Sums s) = NAT by PARTFUN1:def 2;
rng (Partial_Sums s) c= REAL by VALUED_0:def 3;
then Partial_Sums s is Relation of NAT,REAL by A1, RELSET_1:4;
hence Partial_Sums s is Real_Sequence ; :: thesis: verum