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