let A be Ordinal; :: thesis: for B being infinite Cardinal st A in B holds
A +^ B = B
let B be infinite Cardinal; :: thesis: ( A in B implies A +^ B = B )
assume A1: A in B ; :: thesis: A +^ B = B
deffunc H₁( Ordinal) -> set = A +^ $1;
consider fi being Ordinal-Sequence such that
A2: ( dom fi = B & ( for C being Ordinal st C in B holds
fi . C = H₁(C) ) ) from ORDINAL2:sch 3();
A3: A +^ B = sup fi by A2, ORDINAL2:29;

now :: thesis: for D being Ordinal st D in rng fi holds
D in B

let D be Ordinal; :: thesis: ( D in rng fi implies D in B )
assume D in rng fi ; :: thesis: D in B
then consider x being object such that
B1: ( x in dom fi & fi . x = D ) by FUNCT_1:def 3;
reconsider C = x as Ordinal by B1;
( card A in B & card C in B ) by A1, A2, B1, CARD_1:9;
then (card A) +` (card C) in B +` B by CARD_2:96;
then B2: (card A) +` (card C) in card B by CARD_2:75;
D = A +^ C by A2, B1;
then card D = (card A) +` (card C) by CARD_2:13;
hence D in B by B2, CARD_3:43; :: thesis: verum

end;

then sup (rng fi) c= B by ORDINAL2:20;
then A4: sup fi c= B by ORDINAL2:def 5;
B c= A +^ B by ORDINAL3:24;
hence A +^ B = B by A3, A4, XBOOLE_0:def 10; :: thesis: verum