for q being set
for F being Group-like associative multMagma-Family of {q}
for G being Group st F = q .--> G holds
ex HFG being Homomorphism of (product F),G st
( HFG is bijective & ( for x being {b₁} -defined the carrier of b₃ -valued total Function holds HFG . x = Product x ) )