let n be Element of NAT ; :: thesis: for p being XFinSequence holds p | n is XFinSequence
let p be XFinSequence; :: thesis: p | n is XFinSequence
A1: dom (p | n) = (len p) /\ n by RELAT_1:90;
( len p <= n or n <= len p ) ;
then ( dom (p | n) = len p or dom (p | n) = n ) by A1, Th2;
hence p | n is XFinSequence by Th7; :: thesis: verum