I --> P is TolStr-yielding

proof

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

end;

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