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:7; :: thesis: verum

end;

hence for b₁ being ManySortedSet of I st b₁ = I --> P holds
b₁ is pcs-yielding ; :: thesis: verum