let n be Element of 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 ( dom q = (dom p) /\ (Seg n) & Seg (len q) = dom q ) by FINSEQ_1:def 3, RELAT_1:90;
then Seg (len q) c= Seg n by XBOOLE_1:17;
hence len q <= n by FINSEQ_1:7; :: thesis: verum