A: dom ||.s.|| = dom s by Def1
.= NAT by PARTFUN1:def 4 ;
rng ||.s.|| c= REAL by RELAT_1:def 19;
hence ||.s.|| is Real_Sequence by A, FUNCT_2:4; :: thesis: verum