:: deftheorem defines ^* GR_FREE0:def 11 :
for G1, G2 being Group
for b₃ being strict Group holds
( b₃ = G1 ^* G2 iff ex H being Group-like associative multMagma-Family of 2 st
( H = <%G1,G2%> & b₃ = FreeProduct H ) );