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