len p in dom p by FINSEQ_5:6;
hence ( p . (len p) is finite & p . (len p) is NAT -defined ) ; :: thesis: verum