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