take
the set --> the Function
; :: thesis: the set --> the Function is Function-yielding

let x be object ; :: according to FUNCOP_1:def 6 :: thesis: ( x in dom ( the set --> the Function) implies ( the set --> the Function) . x is Function )

thus ( x in dom ( the set --> the Function) implies ( the set --> the Function) . x is Function ) ; :: thesis: verum

let x be object ; :: according to FUNCOP_1:def 6 :: thesis: ( x in dom ( the set --> the Function) implies ( the set --> the Function) . x is Function )

thus ( x in dom ( the set --> the Function) implies ( the set --> the Function) . x is Function ) ; :: thesis: verum