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

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;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