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 q = p | (Seg n) ; :: thesis: len q <= n
then A1: dom q = (dom p) /\ (Seg n) by RELAT_1:61;
Seg (len q) = dom q by Def3;
hence len q <= n by Th5, A1, XBOOLE_1:17; :: thesis: verum