let a be set ; :: according to FUNCOP_1:def 6 :: thesis: ( a in dom (A --> f) implies (A --> f) . a is Function )
thus ( a in dom (A --> f) implies (A --> f) . a is Function ) ; :: thesis: verum