let i be Element of NAT ; :: thesis: for q being XFinSequence st i <= len q holds
len (q | i) = i
let q be XFinSequence; :: thesis: ( i <= len q implies len (q | i) = i )
assume A0: i <= len q ; :: thesis: len (q | i) = i
i c= len q by A0, NAT_1:40;
hence len (q | i) = i by RELAT_1:91; :: thesis: verum