(rng f) \/ (rng g) c= D ;
then rng (f ^ g) c= D by FRX;
then for k being Nat st k in dom (f ^ g) holds
(f ^ g) . k in D by FUNCT_1:3;
hence f ^ g is XFinSequence of D by AFINSQ_2:4; :: thesis: verum