let x be object ; :: according to FINSET_1:def 4 :: thesis: ( not x in dom (F * G) or (F * G) . x is finite )
assume x in dom (F * G) ; :: thesis: (F * G) . x is finite
then (F * G) . x = F . (G . x) by FUNCT_1:12;
hence (F * G) . x is finite ; :: thesis: verum