let f be sequence of D; :: thesis: f is total
thus dom f = NAT by FUNCT_2:def 1; :: according to PARTFUN1:def 2 :: thesis: verum