let p, q be FinSequence; :: thesis: for k, l being natural number st len p = k + l & q = p | (Seg k) holds
dom q = Seg k
let k, l be natural number ; :: thesis: ( len p = k + l & q = p | (Seg k) implies dom q = Seg k )
assume ( len p = k + l & q = p | (Seg k) ) ; :: thesis: dom q = Seg k
then len q = k by Th59;
hence dom q = Seg k by FINSEQ_1:def 3; :: thesis: verum