for G being finite strict commutative Group st card G > 1 holds
ex I being non empty finite set ex F being Group-like associative commutative multMagma-Family of I ex HFG being Homomorphism of (product F),G st
( I = support (prime_factorization (card G)) & ( for p being Element of I holds
( F . p is strict Subgroup of G & card (F . p) = (prime_factorization (card G)) . p ) ) & ( for p, q being Element of I st p <> q holds
the carrier of (F . p) /\ the carrier of (F . q) = {(1_ G)} ) & HFG is bijective & ( for x being b₂ -defined the carrier of b₁ -valued total Function st ( for p being Element of I holds x . p in F . p ) holds
( x in product F & HFG . x = Product x ) ) )