let f, g be FinSequence; :: thesis: dom f c= dom (f ^' g)
len f <= len (f ^' g) by TOPREAL8:7;
hence dom f c= dom (f ^' g) by FINSEQ_3:30; :: thesis: verum