let A be Ordinal; :: thesis: for f being Sequence holds dom (f /^ A) c= dom f
let f be Sequence; :: thesis: dom (f /^ A) c= dom f
0 c= A ;
then ( dom (f /^ A) = (dom f) -^ A & (dom f) -^ A c= (dom f) -^ 0 ) by Def1, ORDINAL3:58;
hence dom (f /^ A) c= dom f by ORDINAL3:56; :: thesis: verum