set f = I --> P;
I --> P is pcs-chain-like

proof

let R, S be pcs-Str ; :: according to PCS_0:def 35 :: thesis: ( R in rng (I --> P) & S in rng (I --> P) & not R c= S implies S c= R )
assume A1: ( R in rng (I --> P) & S in rng (I --> P) ) ; :: thesis: ( R c= S or S c= R )
( I = {} or I <> {} ) ;
then ( rng (I --> P) = {P} or rng (I --> P) = {} ) by FUNCOP_1:14, FUNCOP_1:16;
then ( ( P = R & P = S ) or rng (I --> P) = {} ) by A1, TARSKI:def 1;
hence ( R c= S or S c= R ) by A1; :: thesis: verum

end;

hence I --> P is pcs-chain-like ManySortedSet of I ; :: thesis: verum