let f be non empty FinSequence; :: thesis: for g being FinSequence holds dom g c= dom (f ^' g)
let g be FinSequence; :: thesis: dom g c= dom (f ^' g)
len g <= len (f ^' g) by TOPREAL8:9;
hence dom g c= dom (f ^' g) by FINSEQ_3:30; :: thesis: verum