A1: rng (F * p) c= the carrier of G ;
dom F = FreeAtoms H by FUNCT_2:def 1;
then rng p c= dom F ;
then dom (F * p) = dom p by RELAT_1:27;
then ex k being Nat st dom (F * p) = Seg k by FINSEQ_1:def 2;
then F * p is FinSequence by FINSEQ_1:def 2;
hence p * F is FinSequence of G by A1, FINSEQ_1:def 4; :: thesis: verum