(rng f) \/ (rng g) c= D ;
then rng (f ^ g) c= D by FRX;
hence f ^ g is FinSequence of D by FINSEQ_1:def 4; :: thesis: verum