let k be object ; :: according to FUNCT_1:def 8 :: thesis: ( not k in dom (c (#) f) or (c (#) f) . k is empty )
assume k in dom (c (#) f) ; :: thesis: (c (#) f) . k is empty
then (c (#) f) . k = c * (f . k) by VALUED_1:def 5;
hence (c (#) f) . k is empty ; :: thesis: verum