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 () & ( for p being Element of I holds
( F . p is strict Subgroup of G & card (F . p) = () . 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 b1 -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 b1 -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 () & ( for p being Element of I holds
( F . p is strict Subgroup of G & card (F . p) = () . 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 b1 -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 b1 -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 (),G such that
A1: ( I = support () & ( for p being Element of I holds
( F . p is strict Subgroup of G & card (F . p) = () . 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 ;
then consider x being object such that
A3: ( x in the carrier of () & y = HFG . x ) by FUNCT_2:11;
reconsider x = x as I -defined total Function by ;
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 ;
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 ;
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 () & x2 in the carrier of () ) by ;
hence x1 = x2 by ; :: 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 () & ( for p being Element of I holds
( F . p is strict Subgroup of G & card (F . p) = () . 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 b1 -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 b1 -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