A1: dom ||.s.|| = dom s by Def2
.= NAT by PARTFUN1:def 2 ;
rng ||.s.|| c= REAL by RELAT_1:def 19;
hence ||.s.|| is Real_Sequence by A1, FUNCT_2:2; :: thesis: verum