let x be set ; :: thesis: for k being Nat holds card (k --> x) = k
let k be Nat; :: thesis: card (k --> x) = k
dom (k --> x) = k by FUNCOP_1:13;
hence card (k --> x) = card k by Th62
.= k by Def2 ;
:: thesis: verum