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 Th15
.= (card K) +` (card K) by Th16
.= K +` (card K)
.= K +` K ; :: thesis: verum