A1: dom seq = NAT by FUNCT_2:def 1;
dom (r (#) seq) = dom seq by VFUNCT_1:def 4;
hence r (#) seq is Real_Sequence of N by A1, FUNCT_2:67; :: thesis: verum