let x be object ; :: thesis: for k being Nat holds card (k --> x) = k
let k be Nat; :: thesis: card (k --> x) = k
dom (k --> x) = k ;
hence card (k --> x) = card k by Th60
.= k ;
:: thesis: verum