OuterVx (f,n) c= Seg n by Th28;
hence OuterVx (f,n) is finite ; :: thesis: verum