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