let i be Nat; :: thesis: for q being FinSequence st i <= len q holds
len (q | i) = i
let q be FinSequence; :: thesis: ( i <= len q implies len (q | i) = i )
assume i <= len q ; :: thesis: len (q | i) = i
then Seg i c= Seg (len q) by Th5;
then Seg i c= dom q by Def3;
then ( i in NAT & Seg i = dom (q | i) ) by ORDINAL1:def 12, RELAT_1:62;
hence len (q | i) = i by Def3; :: thesis: verum