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