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