theorem :: GROUP_17:35

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 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)} ) & ( for y being Element of G ex x being b₂ -defined the carrier of b₁ -valued total Function st
( ( for p being Element of I holds x . p in F . p ) & y = Product x ) ) & ( for x1, x2 being b₂ -defined the carrier of b₁ -valued total Function st ( for p being Element of I holds x1 . p in F . p ) & ( for p being Element of I holds x2 . p in F . p ) & Product x1 = Product x2 holds
x1 = x2 ) )