let p, q be FinSequence; :: thesis: for k, l being Nat st len p = k + l & q = p | (Seg k) holds
dom q = Seg k
let k, l be Nat; :: thesis: ( len p = k + l & q = p | (Seg k) implies dom q = Seg k )
assume that
A1: len p = k + l and
A2: q = p | (Seg k) ; :: thesis: dom q = Seg k
len q = k by A1, A2, Th51;
hence dom q = Seg k by FINSEQ_1:def 3; :: thesis: verum