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:88;
hence dom (f | i) c= dom f by RELAT_1:25; :: thesis: verum