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