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