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