A1: ( len p <= n or n <= len p ) ;
dom (p | n) = (len p) /\ n by RELAT_1:61;
then ( dom (p | n) = len p or dom (p | n) = n ) by A1, NAT_1:46;
hence p | n is finite by Th7; :: thesis: verum