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