let f be FinSequence; :: thesis: for i being Nat holds dom (f | i) c= dom f
let i be Nat; :: thesis: dom (f | i) c= dom f
f | i c= f by RELAT_1:59;
hence dom (f | i) c= dom f by RELAT_1:11; :: thesis: verum