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