now :: thesis: for x being object st x in dom (f * g) holds
(f * g) . x is Cardinal
let x be object ; :: thesis: ( x in dom (f * g) implies (f * g) . x is Cardinal )
assume A1: x in dom (f * g) ; :: thesis: (f * g) . x is Cardinal
then ( x in dom g & g . x in dom f ) by FUNCT_1:11;
then f . (g . x) is Cardinal by CARD_3:def 1;
hence (f * g) . x is Cardinal by A1, FUNCT_1:12; :: thesis: verum
end;
hence f * g is Cardinal-yielding by CARD_3:def 1; :: thesis: verum