let a be Aleph; :: thesis:
nextcard a is_cofinal_with cf (nextcard a) by Def1;
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 ;
A4: ( card (Union xi) c= Sum (Card xi) & Sum ((cf (nextcard a)) --> a) = (cf (nextcard a)) *` a ) by CARD_2:65, CARD_3:39;
A5: ( card (nextcard a) = nextcard a & succ (Union xi) = (Union xi) +^ 1 ) by ORDINAL2:31;

A6: now :: thesis:

let x be object ; :: thesis:
assume A7: x in cf (nextcard a) ; :: thesis:
xi . x in rng xi by A1, A7, FUNCT_1:def 3;
then A8: card (xi . x) in nextcard a by A2, CARD_1:8, ORDINAL1:12;
( (Card xi) . x = card (xi . x) & ((cf (nextcard a)) --> a) . x = a ) by A1, A7, CARD_3:def 2, FUNCOP_1:7;
hence (Card xi) . x c= ((cf (nextcard a)) --> a) . x by A8, CARD_3:91; :: thesis:

end;

( dom (Card xi) = dom xi & dom ((cf (nextcard a)) --> a) = cf (nextcard a) ) by CARD_3:def 2;
then Sum (Card xi) c= Sum ((cf (nextcard a)) --> a) by A1, A6, CARD_3:30;
then card (Union xi) c= (cf (nextcard a)) *` a by A4;
then A9: (card (Union xi)) +` 1 c= ((cf (nextcard a)) *` a) +` 1 by CARD_2:84;
A10: card ((Union xi) +^ 1) = (card (Union xi)) +` (card 1) by CARD_2:13;
ex A being Ordinal st rng xi c= A by ORDINAL2:def 4;
then On (rng xi) = rng xi by ORDINAL3:6;
then A11: card (nextcard a) c= card (succ (Union xi)) by A3, CARD_1:11, ORDINAL3:72;
A12: cf (nextcard a) c= nextcard a by Def1;

now :: thesis:

per cases ;

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

then A13: (cf (nextcard a)) *` a = 0 by CARD_2:20;
thus cf (nextcard a) = nextcard a by A11, A5, A9, A10, A13; :: thesis:

end;

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

0 c= cf (nextcard a) ;
then A15: 0 in cf (nextcard a) by A14, CARD_1:3;
A16: ( cf (nextcard a) c= a or a c= cf (nextcard a) ) ;
1 in a by Lm1, Th15;
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, Th17, CARD_1:18, CARD_2:76, CARD_4:16;
then ( nextcard a c= (cf (nextcard a)) +` 1 & 1 in cf (nextcard a) ) by A11, A5, A9, A10, Th15, CARD_1:4;
then nextcard a c= cf (nextcard a) by A11, A5, A9, A10, A17, CARD_1:4, CARD_2:76;
hence cf (nextcard a) = nextcard a by A12; :: thesis:

end;

end;

end;

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