let n be Nat; :: thesis: for p being XFinSequence holds len (p | n) <= n
let p be XFinSequence; :: thesis: len (p | n) <= n
dom (p | n) c= n by RELAT_1:87;
hence len (p | n) <= n by NAT_1:40; :: thesis: verum