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) and
A2: rng xi c= nextcard a and
xi is increasing and
A3: nextcard a = sup xi by ORDINAL2:def 21;
A4: ( card (Union xi) c= Sum (Card xi) & Sum ((cf (nextcard a)) --> a) = (cf (nextcard a)) *` a ) by CARD_3:52, CARD_3:54;
A5: ( card (nextcard a) = nextcard a & succ (Union xi) = (Union xi) +^ 1 ) by CARD_1:def 5, ORDINAL2:48;

A6: now

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

end;

( dom (Card xi) = dom xi & dom ((cf (nextcard a)) --> a) = cf (nextcard a) ) by CARD_3:def 2, FUNCOP_1:19;
then Sum (Card xi) c= Sum ((cf (nextcard a)) --> a) by A1, A6, CARD_3:43;
then card (Union xi) c= (cf (nextcard a)) *` a by A4, XBOOLE_1:1;
then A9: (card (Union xi)) +` 1 c= ((cf (nextcard a)) *` a) +` 1 by CARD_3:126;
A10: card ((Union xi) +^ 1) = (card (Union xi)) +` (card 1) by CARD_2:24;
ex A being Ordinal st rng xi c= A by ORDINAL2:def 8;
then On (rng xi) = rng xi by ORDINAL3:8;
then A11: card (nextcard a) c= card (succ (Union xi)) by A3, CARD_1:27, ORDINAL3:85;
A12: cf (nextcard a) c= nextcard a by Def2;

now

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

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

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

end;

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

0 c= cf (nextcard a) by XBOOLE_1:2;
then A15: 0 in cf (nextcard a) by A14, CARD_1:13;
A16: ( cf (nextcard a) c= a or a c= cf (nextcard a) ) ;
1 in a by Lm1, Th25;
then A17: ( ( (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 A15, A16, Th27, CARD_1:32, CARD_3:118, CARD_4:78;
then ( nextcard a c= (cf (nextcard a)) +` 1 & 1 in cf (nextcard a) ) by A11, A5, A9, A10, Lm1, Th25, CARD_1:14, XBOOLE_1:1;
then nextcard a c= cf (nextcard a) by A11, A5, A9, A10, A17, Lm1, CARD_1:14, CARD_3:118;
hence cf (nextcard a) = nextcard a by A12, XBOOLE_0:def 10; :: thesis: verum

end;

end;

end;

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