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