per cases ( rng F is empty or not rng F is empty ) ;

suppose rng F is empty ; :: thesis: F * P is Sequence-like

then F = {} ;
hence F * P is Sequence-like ; :: thesis: verum

end;

suppose A1: not rng F is empty ; :: thesis: F * P is Sequence-like

A2: dom P = dom F by FUNCT_2:52;
F is Function of (dom F),(rng F) by FUNCT_2:1;
then dom (F * P) = dom F by A1, FUNCT_2:123, A2;
hence F * P is Sequence-like by ORDINAL1:def 7; :: thesis: verum

end;

end;