consider f being Function;
dom (I --> f) = I by FUNCOP_1:19;
then reconsider F = I --> f as ManySortedSet of I by PARTFUN1:def 4;
take F ; :: thesis: F is Function-yielding
let x be set ; :: according to FUNCOP_1:def 6 :: thesis: ( not x in proj1 F or F . x is set )
assume x in dom F ; :: thesis: F . x is set
thus F . x is set ; :: thesis: verum