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