let K be Cardinal; :: thesis: K *` 1 = K
K = card K by CARD_1:def 2;
hence K *` 1 = K by Th13, ORDINAL3:15; :: thesis: verum