let G be Group; :: thesis: ( G is trivial implies G is free-abelian )
assume A1: G is trivial ; :: thesis: G is free-abelian
set c = the empty Cardinal;
take the empty Cardinal ; :: according to GR_FREE0:def 13 :: thesis: G, sum ( the empty Cardinal --> INT.Group) are_isomorphic
sum ( the empty Cardinal --> INT.Group) = product ( the empty Cardinal --> INT.Group) by GROUP_7:9;
hence G, sum ( the empty Cardinal --> INT.Group) are_isomorphic by A1, GROUP_6:69; :: thesis: verum