for q being set
for F being Group-like associative multMagma-Family of {q}
for G being Group st F = q .--> G holds
ex I being Homomorphism of G,(product F) st
( I is bijective & ( for x being Element of G holds I . x = q .--> x ) )