A1: ( dom seq1 = NAT & dom seq2 = NAT ) by FUNCT_2:def 1;
dom (seq1 + seq2) = (dom seq1) /\ (dom seq2) by VFUNCT_1:def 1;
hence seq1 + seq2 is Real_Sequence of N by A1, FUNCT_2:67; :: thesis: verum