for x being object st x in NAT holds
|.p.| . x in the carrier of INT.Ring by INT_1:def 1;
hence |.p.| is sequence of INT.Ring by A1, FUNCT_2:3; :: thesis: verum