consider f being Function, I being set ;
A1: dom (I --> f) = I by Th19;
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 )
thus ( x in dom F implies F . x is Function ) by A1, Th13; :: thesis: verum