A1: dom seq = NAT by FUNCT_2:def 1;
dom (- seq) = dom seq by VFUNCT_1:def 6;
hence - seq is Real_Sequence of N by A1, FUNCT_2:130; :: thesis: verum