let i be natural Number ; :: thesis: for p, q being FinSequence st q = p | (Seg i) & len p <= i holds
p = q
let p, q be FinSequence; :: thesis: ( q = p | (Seg i) & len p <= i implies p = q )
assume A1: q = p | (Seg i) ; :: thesis: ( not len p <= i or p = q )
assume len p <= i ; :: thesis: p = q
then Seg (len p) c= Seg i by FINSEQ_1:5;
then dom p c= Seg i by FINSEQ_1:def 3;
hence p = q by A1, RELAT_1:68; :: thesis: verum