let i be Nat; :: thesis: for q being FinSequence st len q <= i holds
q | i = q
let q be FinSequence; :: thesis: ( len q <= i implies q | i = q )
assume len q <= i ; :: thesis: q | i = q
then Seg (len q) c= Seg i by Th5;
then dom q c= Seg i by Def3;
hence q | i = q by RELAT_1:68; :: thesis: verum