ff | X is Cardinal-yielding
proof
let x be object ; :: according to CARD_3:def 1 :: thesis: ( x in dom (ff | X) implies (ff | X) . x is Cardinal )
assume A1: x in dom (ff | X) ; :: thesis: (ff | X) . x is Cardinal
then A2: (ff | X) . x = ff . x by FUNCT_1:47;
dom (ff | X) = (dom ff) /\ X by RELAT_1:61;
then x in dom ff by A1, XBOOLE_0:def 4;
hence (ff | X) . x is Cardinal by A2, Def1; :: thesis: verum
end;
hence ff | X is Cardinal-yielding ; :: thesis: verum