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