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