let G be Group; :: thesis: ( G is trivial implies G is free )
assume A1: G is trivial ; :: thesis: G is free
set c = the empty Cardinal;
take the empty Cardinal ; :: according to GR_FREE0:def 12 :: thesis: G, FreeProduct ( the empty Cardinal --> INT.Group) are_isomorphic
thus G, FreeProduct ( the empty Cardinal --> INT.Group) are_isomorphic by A1, GROUP_6:69; :: thesis: verum