let i be Element of NAT ; :: thesis: for q being XFinSequence holds len (q | i) <= i
let q be XFinSequence; :: thesis: len (q | i) <= i
dom (q | i) c= i by RELAT_1:87;
hence len (q | i) <= i by NAT_1:40; :: thesis: verum