now :: thesis: for x being object st x in dom <%c1%> holds
<%c1%> . x is Cardinal

let x be object ; :: thesis: ( x in dom <%c1%> implies <%c1%> . x is Cardinal )
assume x in dom <%c1%> ; :: thesis: <%c1%> . x is Cardinal
then x in {0} by AFINSQ_1:def 4, CARD_1:49;
then x = 0 by TARSKI:def 1;
hence <%c1%> . x is Cardinal ; :: thesis: verum

end;

hence <%c1%> is Cardinal-yielding by CARD_3:def 1; :: thesis: verum