set f = the Function;
reconsider F = I --> the Function as ManySortedSet of I ;
take F ; :: thesis: F is Function-yielding
let x be object ; :: according to FUNCOP_1:def 6 :: thesis: ( not x in dom F or F . x is set )
assume x in dom F ; :: thesis: F . x is set
thus F . x is set ; :: thesis: verum