I --> P is pcs-yielding

proof

let i be set ; :: according to PCS_0:def 33 :: thesis: ( i in I implies (I --> P) . i is pcs )
thus ( i in I implies (I --> P) . i is pcs ) by FUNCOP_1:13; :: thesis: verum

end;

hence I --> P is V217 ManySortedSet of I ; :: thesis: verum