let X be set ; :: thesis: card (id X) = card X
id X in Funcs (X,X) by FUNCT_2:9;
hence card (id X) = card X by CARD_2:3; :: thesis: verum