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 k c= len p by NAT_1:39;
hence dom (p | k) = k by RELAT_1:62; :: thesis: verum