let n be Nat; :: thesis: for p, q being FinSequence st q = p | (Seg n) holds
len q <= n
let p, q be FinSequence; :: thesis: ( q = p | (Seg n) implies len q <= n )
assume A1: q = p | (Seg n) ; :: thesis: len q <= n
A2: dom q = (dom p) /\ (Seg n) by A1, RELAT_1:90;
A3: Seg (len q) = dom q by Def3;
A4: Seg (len q) c= Seg n by A2, A3, XBOOLE_1:17;
thus len q <= n by A4, Th7; :: thesis: verum