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