let K be Cardinal; :: thesis: 2 *` K = K +` K
thus 2 *` K = card ([:{{}},K:] \/ [:{1},K:]) by CARD_1:50, ZFMISC_1:109
.= card ([:K,{{}}:] \/ [:K,{1}:]) by Th27
.= (card K) +` (card K) by Th28
.= K +` (card K) by CARD_1:def 2
.= K +` K by CARD_1:def 2 ; :: thesis: verum