consider n1 being Nat such that
A1: dom F1 = Seg n1 by FINSEQ_1:def 2;
take n1 ; :: according to FINSEQ_1:def 2 :: thesis: dom (F * F1) = Seg n1
( dom F = REAL & rng F1 c= REAL ) by FUNCT_2:def 1;
hence dom (F * F1) = Seg n1 by A1, RELAT_1:27; :: thesis: verum