dom p = Seg (len p) by Def3;
hence dom p is Subset of NAT ; :: thesis: verum