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 I --> P is V207 ManySortedSet of I ; :: thesis: verum