let G be finite strict commutative Group; :: thesis: ( card G > 1 implies 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 G -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 G -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 ) ) )
assume card G > 1 ; :: thesis: 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 G -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 G -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 ) )
then consider I being non empty finite set , F being Group-like associative commutative multMagma-Family of I, HFG being Homomorphism of (product F),G such that
A1: ( 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 I -defined the carrier of G -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 ) ) ) by Th34;
A2: for y being Element of G ex x being I -defined the carrier of G -valued total Function st
( ( for p being Element of I holds x . p in F . p ) & y = Product x )

proof

let y be Element of G; :: thesis: ex x being I -defined the carrier of G -valued total Function st
( ( for p being Element of I holds x . p in F . p ) & y = Product x )
y in the carrier of G ;
then y in rng HFG by A1, FUNCT_2:def 3;
then consider x being object such that
A3: ( x in the carrier of (product F) & y = HFG . x ) by FUNCT_2:11;
reconsider x = x as I -defined total Function by A3, Lm6;
A4: for p being Element of I holds x . p in F . p

proof

let p be Element of I; :: thesis: x . p in F . p
consider R being non empty multMagma such that
A5: ( R = F . p & x . p in the carrier of R ) by Lm7, A3;
thus x . p in F . p by A5; :: thesis: verum

end;

rng x c= the carrier of G

proof

let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in rng x or y in the carrier of G )
assume y in rng x ; :: thesis: y in the carrier of G
then consider i being object such that
A6: ( i in dom x & y = x . i ) by FUNCT_1:def 3;
reconsider i = i as Element of I by A6;
consider R being non empty multMagma such that
A7: ( R = F . i & x . i in the carrier of R ) by A3, Lm7;
F . i is strict Subgroup of G by A1;
then the carrier of (F . i) c= the carrier of G by GROUP_2:def 5;
hence y in the carrier of G by A6, A7; :: thesis: verum

end;

then reconsider x = x as I -defined the carrier of G -valued total Function by RELAT_1:def 19;
take x ; :: thesis: ( ( for p being Element of I holds x . p in F . p ) & y = Product x )
thus ( ( for p being Element of I holds x . p in F . p ) & y = Product x ) by A1, A3, A4; :: thesis: verum

end;

now :: thesis: for x1, x2 being I -defined the carrier of G -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

let x1, x2 be I -defined the carrier of G -valued total Function; :: thesis: ( ( 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 implies x1 = x2 )
assume A8: ( ( 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 ) ; :: thesis: x1 = x2
( x1 in product F & HFG . x1 = Product x1 ) by A8, A1;
then A9: HFG . x1 = HFG . x2 by A8, A1;
( x1 in the carrier of (product F) & x2 in the carrier of (product F) ) by A8, A1, STRUCT_0:def 5;
hence x1 = x2 by A9, A1, FUNCT_2:19; :: thesis: verum

end;

hence 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 G -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 G -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 ) ) by A1, A2; :: thesis: verum