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