let x be set ; :: according to CARD_FIN:def 3 :: thesis: (F * G) . x is finite

per cases ( x in dom (F * G) or not x in dom (F * G) ) ;

suppose 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

end;

suppose not x in dom (F * G) ; :: thesis: (F * G) . x is finite

hence (F * G) . x is finite by FUNCT_1:def 2; :: thesis: verum

end;

end;