set I = 1;
take 1 ; :: according to GR_FREE0:def 12 :: thesis: INT.Group , FreeProduct (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, FreeProduct (I9 --> INT.Group) are_isomorphic by A2, Th58;
hence INT.Group , FreeProduct (1 --> INT.Group) are_isomorphic ; :: thesis: verum