consider f being Function, I being set ;
take I --> f ; :: thesis: I --> f is Function-yielding
let x be set ; :: according to FUNCOP_1:def 6 :: thesis: ( x in dom (I --> f) implies (I --> f) . x is Function )
dom (I --> f) = I by Th19;
hence ( x in dom (I --> f) implies (I --> f) . x is Function ) by Th13; :: thesis: verum