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