set I = 1;
take 1 ; :: according to GR_FREE0:def 13 :: thesis: INT.Group , sum (1 --> INT.Group) are_isomorphic
reconsider I9 = 1 as non empty set ;
A2: 1 = {0} by CARD_1:49;
then reconsider i = 0 as Element of I9 by TARSKI:def 1;
(I9 --> INT.Group) . i, product (I9 --> INT.Group) are_isomorphic by A2, Th6;
hence INT.Group , sum (1 --> INT.Group) are_isomorphic by GROUP_7:9; :: thesis: verum