now :: thesis: for x being object st x in dom (A ^ B) holds
(A ^ B) . x is Cardinal

let x be object ; :: thesis: ( x in dom (A ^ B) implies (A ^ B) . b₁ is Cardinal )
assume A1: x in dom (A ^ B) ; :: thesis: (A ^ B) . b₁ is Cardinal
then reconsider c = x as Ordinal ;

per cases ( c in dom A or not c in dom A ) ;

suppose A2: c in dom A ; :: thesis: (A ^ B) . b₁ is Cardinal

then (A ^ B) . c = A . c by ORDINAL4:def 1;
hence (A ^ B) . x is Cardinal by A2, CARD_3:def 1; :: thesis: verum

end;

suppose not c in dom A ; :: thesis: (A ^ B) . b₁ is Cardinal

then consider d being Ordinal such that
A3: c = (dom A) +^ d by ORDINAL1:16, ORDINAL3:27;
c in (dom A) +^ (dom B) by A1, ORDINAL4:def 1;
then A4: d in dom B by A3, ORDINAL3:22;
then (A ^ B) . ((dom A) +^ d) = B . d by ORDINAL4:def 1;
hence (A ^ B) . x is Cardinal by A3, A4, CARD_3:def 1; :: thesis: verum

end;

end;

end;

hence A ^ B is Cardinal-yielding by CARD_3:def 1; :: thesis: verum