let G be Group; :: thesis: card ((1). G) = 1
the carrier of ((1). G) = {(1_ G)} by Def7;
hence card ((1). G) = 1 by CARD_1:30; :: thesis: verum