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