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