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