let i be object ; :: according to FUNCOP_1:def 6 :: thesis: ( i in dom (f | C) implies (f | C) . i is Function )
f . i is Function ;
hence ( i in dom (f | C) implies (f | C) . i is Function ) by FUNCT_1:47; :: thesis: verum