let a be Aleph; :: thesis: cf (nextcard a) = nextcard a
nextcard a is_cofinal_with cf (nextcard a) by Def2;
then consider xi being Ordinal-Sequence such that
A1: ( dom xi = cf (nextcard a) & rng xi c= nextcard a & xi is increasing & nextcard a = sup xi ) by ORDINAL2:def 21;
A2: ( dom (Card xi) = dom xi & dom ((cf (nextcard a)) --> a) = cf (nextcard a) ) by CARD_3:def 2, FUNCOP_1:19;

now

let x be set ; :: thesis: ( x in cf (nextcard a) implies (Card xi) . x c= ((cf (nextcard a)) --> a) . x )
assume Z: x in cf (nextcard a) ; :: thesis: (Card xi) . x c= ((cf (nextcard a)) --> a) . x
then A3: ( (Card xi) . x = card (xi . x) & ((cf (nextcard a)) --> a) . x = a & xi . x in rng xi ) by A1, CARD_3:def 2, FUNCOP_1:13, FUNCT_1:def 5;
reconsider A = xi . x as Ordinal by Z;
card (xi . x) in nextcard a by A1, A3, CARD_1:24, ORDINAL1:22;
hence (Card xi) . x c= ((cf (nextcard a)) --> a) . x by A3, CARD_3:108; :: thesis: verum

end;

then A4: ( card (Union xi) c= Sum (Card xi) & Sum (Card xi) c= Sum ((cf (nextcard a)) --> a) & Sum ((cf (nextcard a)) --> a) = (cf (nextcard a)) *` a ) by A1, A2, CARD_3:43, CARD_3:52, CARD_3:54;
ex A being Ordinal st rng xi c= A by ORDINAL2:def 8;
then ( On (rng xi) = rng xi & sup (rng xi) c= succ (union (On (rng xi))) & union (rng xi) = Union xi & card (Union xi) c= (cf (nextcard a)) *` a & sup (rng xi) = sup xi ) by A4, ORDINAL3:8, ORDINAL3:85, XBOOLE_1:1;
then A5: ( card (nextcard a) c= card (succ (Union xi)) & card (nextcard a) = nextcard a & succ (Union xi) = (Union xi) +^ 1 & (card (Union xi)) +` 1 c= ((cf (nextcard a)) *` a) +` 1 & card ((Union xi) +^ 1) = (card (Union xi)) +` (card 1) ) by A1, CARD_1:27, CARD_1:def 5, CARD_2:24, CARD_3:126, ORDINAL2:48;
then A6: ( nextcard a c= ((cf (nextcard a)) *` a) +` 1 & cf (nextcard a) c= nextcard a ) by Def2, Lm4, XBOOLE_1:1;

now

per cases ( cf (nextcard a) = 0 or cf (nextcard a) <> 0 ) ;

suppose cf (nextcard a) = 0 ; :: thesis: cf (nextcard a) = nextcard a

then ( (cf (nextcard a)) *` a = 0 & 0 +` 1 = 1 & 1 in nextcard a ) by Lm1, Th25, CARD_2:29, CARD_2:32;
hence cf (nextcard a) = nextcard a by A5, Lm4, CARD_1:14; :: thesis: verum

end;

suppose A8: cf (nextcard a) <> 0 ; :: thesis: cf (nextcard a) = nextcard a

0 c= cf (nextcard a) by XBOOLE_1:2;
then ( 0 in cf (nextcard a) & 1 in a & ( cf (nextcard a) c= a or a c= cf (nextcard a) ) ) by A8, Lm1, Th25, CARD_1:13;
then ( ( (cf (nextcard a)) *` a = a & a +` 1 = a & a in nextcard a ) or ( (cf (nextcard a)) *` a = cf (nextcard a) & cf (nextcard a) is Aleph ) ) by Th26, Th27, CARD_1:32, CARD_3:118, CARD_4:78;
then ( nextcard a c= (cf (nextcard a)) +` 1 & cf (nextcard a) is Aleph & 1 in cf (nextcard a) ) by A5, Lm1, Th25, CARD_1:14, XBOOLE_1:1;
then nextcard a c= cf (nextcard a) by CARD_3:118;
hence cf (nextcard a) = nextcard a by A6, XBOOLE_0:def 10; :: thesis: verum

end;

end;

end;

hence cf (nextcard a) = nextcard a ; :: thesis: verum