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