let x be set ; :: thesis: for k being natural number holds card (k --> x) = k
let k be natural number ; :: thesis: card (k --> x) = k
dom (k --> x) = k by FUNCOP_1:13;
hence card (k --> x) = card k by Th104
.= k by Def5 ;
:: thesis: verum