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