rng (F1 ^ F2) = (rng F1) \/ (rng F2) by FINSEQ_1:31;
hence rng (F1 ^ F2) c= X ; :: according to RELAT_1:def 19 :: thesis: verum