let n be Nat; :: thesis: for p, q being FinSequence st q = p | (Seg n) holds
len q <= len p
let p, q be FinSequence; :: thesis: ( q = p | (Seg n) implies len q <= len p )
assume q = p | (Seg n) ; :: thesis: len q <= len p
then A1: dom q = (dom p) /\ (Seg n) by RELAT_1:61;
( Seg (len q) = dom q & Seg (len p) = dom p ) by Def3;
hence len q <= len p by Th5, A1, XBOOLE_1:17; :: thesis: verum