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