let f, g be FinSequence; :: thesis: dom g c= dom (f ^ g)
len g <= (len f) + (len g) by NAT_1:11;
then Seg (len g) c= Seg ((len f) + (len g)) by FINSEQ_1:5;
then dom g c= Seg ((len f) + (len g)) by FINSEQ_1:def 3;
hence dom g c= dom (f ^ g) by FINSEQ_1:def 7; :: thesis: verum