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