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_{1} -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_{1} -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_{1} -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_{1} -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 )

( 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_{1} -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_{1} -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

( 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

( ( for p being Element of I holds x . p in F . p ) & y = Product x ) ) & ( for x1, x2 being b

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

( ( for p being Element of I holds x . p in F . p ) & y = Product x ) ) & ( for x1, x2 being b

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

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;( ( 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

rng x c= the carrier of G
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;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

proof

then reconsider x = x as I -defined the carrier of G -valued total Function by RELAT_1:def 19;
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;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

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

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

hence
ex I being non empty finite set ex F being Group-like associative commutative multMagma-Family of I st 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;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

( 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

( ( for p being Element of I holds x . p in F . p ) & y = Product x ) ) & ( for x1, x2 being b

x1 = x2 ) ) by A1, A2; :: thesis: verum