defpred S₁[ Nat] means for G being finite strict commutative Group st card (support (prime_factorization (card G))) = $1 & $1 <> 0 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 ) ) );
A1: S₁[ 0 ] ;
A2: for n being Nat st S₁[n] holds
S₁[n + 1]

proof

let n be Nat; :: thesis: ( S₁[n] implies S₁[n + 1] )
assume A3: S₁[n] ; :: thesis: S₁[n + 1]
thus S₁[n + 1] :: thesis: verum

proof

let G be finite strict commutative Group; :: thesis: ( card (support (prime_factorization (card G))) = n + 1 & n + 1 <> 0 implies 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 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 ) ) ) )
assume A4: ( card (support (prime_factorization (card G))) = n + 1 & n + 1 <> 0 ) ; :: thesis: 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 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 ) ) )

per cases ( n = 0 or n <> 0 ) ;

suppose A5: n = 0 ; :: thesis: 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 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 ) ) )

set f = prime_factorization (card G);
A6: support (prime_factorization (card G)) = support (pfexp (card G)) by NAT_3:def 9;
support (prime_factorization (card G)) <> {} by A4;
then consider q being object such that
A7: q in support (prime_factorization (card G)) by XBOOLE_0:def 1;
reconsider q = q as Prime by A6, A7, NAT_3:34;
card {q} = 1 by CARD_1:30;
then consider q0 being object such that
A8: support (prime_factorization (card G)) = {q0} by CARD_1:29, A5, A4;
A9: {q} = support (prime_factorization (card G)) by A8, TARSKI:def 1, A7;
reconsider Gq = q |^ (q |-count (card G)) as non zero Nat ;
set g = prime_factorization Gq;
A10: Product (prime_factorization Gq) = Gq by NAT_3:61;
q |-count (card G) <> 0

proof

assume q |-count (card G) = 0 ; :: thesis: contradiction
then (prime_factorization (card G)) . q = 0 by NAT_3:55;
hence contradiction by A7, PRE_POLY:def 7; :: thesis: verum

end;

then A11: support (pfexp Gq) = {q} by NAT_3:42;
then q in support (pfexp Gq) by TARSKI:def 1;
then A12: (prime_factorization Gq) . q = q |^ (q |-count Gq) by NAT_3:def 9;
support (prime_factorization Gq) = {q} by A11, NAT_3:def 9;
then A13: support (prime_factorization Gq) = support (pfexp (card G)) by A9, NAT_3:def 9;
for p being Nat st p in support (pfexp (card G)) holds
(prime_factorization Gq) . p = p |^ (p |-count (card G))

proof

let p be Nat; :: thesis: ( p in support (pfexp (card G)) implies (prime_factorization Gq) . p = p |^ (p |-count (card G)) )
assume p in support (pfexp (card G)) ; :: thesis: (prime_factorization Gq) . p = p |^ (p |-count (card G))
then p in {q} by NAT_3:def 9, A9;
then p = q by TARSKI:def 1;
hence (prime_factorization Gq) . p = p |^ (p |-count (card G)) by A12, NAT_3:25, INT_2:def 4; :: thesis: verum

end;

then A14: Gq = Product (prime_factorization (card G)) by A13, NAT_3:def 9, A10
.= card G by NAT_3:61 ;
reconsider I = {q} as non empty finite set ;
set F = q .--> G;
reconsider F = q .--> G as multMagma-Family of I ;
A16: for s, t being Element of I st s <> t holds
the carrier of (F . s) /\ the carrier of (F . t) = {(1_ G)}

proof

let s, t be Element of I; :: thesis: ( s <> t implies the carrier of (F . s) /\ the carrier of (F . t) = {(1_ G)} )
s = q by TARSKI:def 1;
hence ( s <> t implies the carrier of (F . s) /\ the carrier of (F . t) = {(1_ G)} ) by TARSKI:def 1; :: thesis: verum

end;

A18: for x being Element of I holds
( F . x is strict Subgroup of G & card (F . x) = (prime_factorization (card G)) . x )

proof

let x be Element of I; :: thesis: ( F . x is strict Subgroup of G & card (F . x) = (prime_factorization (card G)) . x )
x in support (prime_factorization (card G)) by TARSKI:def 1, A7;
then A20: x in support (pfexp (card G)) by NAT_3:def 9;
A21: x = q by TARSKI:def 1;
card (F . x) = card G
.= (prime_factorization (card G)) . x by A21, A20, NAT_3:def 9, A14 ;
hence ( F . x is strict Subgroup of G & card (F . x) = (prime_factorization (card G)) . x ) by GROUP_2:54; :: thesis: verum

end;

reconsider F = F as Group-like associative commutative multMagma-Family of I ;
take I ; :: thesis: 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 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 ) ) )
take F ; :: thesis: 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 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 ) ) )
consider HFG being Homomorphism of (product F),G such that
A24: ( HFG is bijective & ( for x being {q} -defined the carrier of G -valued total Function holds HFG . x = Product x ) ) by Th26;
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 A24, Th25;
hence 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 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 A9, A24, A16, A18; :: thesis: verum

end;

suppose A25: n <> 0 ; :: thesis: 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 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 ) ) )

set f = prime_factorization (card G);
A26: Product (prime_factorization (card G)) = card G by NAT_3:61;
A27: support (prime_factorization (card G)) = support (pfexp (card G)) by NAT_3:def 9;
support (prime_factorization (card G)) <> {} by A4;
then consider q being object such that
A28: q in support (prime_factorization (card G)) by XBOOLE_0:def 1;
reconsider q = q as Prime by A27, A28, NAT_3:34;
reconsider Gq = q |^ (q |-count (card G)) as non zero Nat ;
set g = prime_factorization Gq;
set h = (prime_factorization (card G)) -' (prime_factorization Gq);
q |-count (card G) <> 0

proof

assume q |-count (card G) = 0 ; :: thesis: contradiction
then (prime_factorization (card G)) . q = 0 by NAT_3:55;
hence contradiction by A28, PRE_POLY:def 7; :: thesis: verum

end;

then A29: support (pfexp Gq) = {q} by NAT_3:42;
then q in support (pfexp Gq) by TARSKI:def 1;
then A30: (prime_factorization Gq) . q = q |^ (q |-count Gq) by NAT_3:def 9;
A31: (prime_factorization Gq) . q = q |^ (q |-count (card G)) by NAT_3:25, INT_2:def 4, A30;
A32: support (prime_factorization Gq) = {q} by A29, NAT_3:def 9;
A33: for x being object holds
( x in support ((prime_factorization (card G)) -' (prime_factorization Gq)) iff x in (support (prime_factorization (card G))) \ {q} )

proof

let x be object ; :: thesis: ( x in support ((prime_factorization (card G)) -' (prime_factorization Gq)) iff x in (support (prime_factorization (card G))) \ {q} )

hereby :: thesis: ( x in (support (prime_factorization (card G))) \ {q} implies x in support ((prime_factorization (card G)) -' (prime_factorization Gq)) )

assume A34: x in support ((prime_factorization (card G)) -' (prime_factorization Gq)) ; :: thesis: x in (support (prime_factorization (card G))) \ {q}
then A35: x in support (prime_factorization (card G)) by PRE_POLY:39, TARSKI:def 3;
then A36: x in support (pfexp (card G)) by NAT_3:def 9;
not x in {q}

proof

assume x in {q} ; :: thesis: contradiction
then A37: x = q by TARSKI:def 1;
((prime_factorization (card G)) -' (prime_factorization Gq)) . x = ((prime_factorization (card G)) . x) -' ((prime_factorization Gq) . x) by PRE_POLY:def 6
.= (q |^ (q |-count (card G))) -' ((prime_factorization Gq) . q) by A37, A36, NAT_3:def 9
.= (q |^ (q |-count (card G))) -' (q |^ (q |-count (card G))) by NAT_3:25, INT_2:def 4, A30
.= (q |^ (q |-count (card G))) - (q |^ (q |-count (card G))) by XREAL_0:def 2
.= 0 ;
hence contradiction by A34, PRE_POLY:def 7; :: thesis: verum

end;

hence x in (support (prime_factorization (card G))) \ {q} by XBOOLE_0:def 5, A35; :: thesis: verum

end;

assume x in (support (prime_factorization (card G))) \ {q} ; :: thesis: x in support ((prime_factorization (card G)) -' (prime_factorization Gq))
then A38: ( x in support (prime_factorization (card G)) & not x in {q} ) by XBOOLE_0:def 5;
x in support (pfexp (card G)) by A38, NAT_3:def 9;
then reconsider x0 = x as Prime by NAT_3:34;
A39: ((prime_factorization (card G)) -' (prime_factorization Gq)) . x0 = ((prime_factorization (card G)) . x0) -' ((prime_factorization Gq) . x0) by PRE_POLY:def 6;
A40: (prime_factorization Gq) . x0 = 0 by A38, A32, PRE_POLY:def 7;
(prime_factorization (card G)) . x0 <> 0 by A38, PRE_POLY:def 7;
then ((prime_factorization (card G)) -' (prime_factorization Gq)) . x <> 0 by A39, A40, NAT_D:40;
hence x in support ((prime_factorization (card G)) -' (prime_factorization Gq)) by PRE_POLY:def 7; :: thesis: verum

end;

then A41: support ((prime_factorization (card G)) -' (prime_factorization Gq)) = (support (prime_factorization (card G))) \ {q} by TARSKI:2;
then A42: support ((prime_factorization (card G)) -' (prime_factorization Gq)) misses support (prime_factorization Gq) by A32, XBOOLE_1:79;
reconsider h = (prime_factorization (card G)) -' (prime_factorization Gq) as bag of SetPrimes ;
A43: for x being Prime st x in support h holds
ex n being Nat st
( 0 < n & h . x = x |^ n )

proof

let x be Prime; :: thesis: ( x in support h implies ex n being Nat st
( 0 < n & h . x = x |^ n ) )
assume x in support h ; :: thesis: ex n being Nat st
( 0 < n & h . x = x |^ n )
then A44: ( x in support (prime_factorization (card G)) & not x in {q} ) by XBOOLE_0:def 5, A41;
A45: h . x = ((prime_factorization (card G)) . x) -' ((prime_factorization Gq) . x) by PRE_POLY:def 6;
(prime_factorization Gq) . x = 0 by A44, A32, PRE_POLY:def 7;
then h . x = (prime_factorization (card G)) . x by A45, NAT_D:40;
hence ex n being Nat st
( 0 < n & h . x = x |^ n ) by A44, INT_7:def 1; :: thesis: verum

end;

then A46: h is prime-factorization-like by INT_7:def 1;
A47: {q} c= support (prime_factorization (card G)) by A28, ZFMISC_1:31;
A48: support h c= support (prime_factorization (card G)) by XBOOLE_1:36, A41;
A49: (support h) \/ {q} = support (prime_factorization (card G)) by A28, ZFMISC_1:31, A41, XBOOLE_1:45;
for x being object st x in SetPrimes holds
(prime_factorization (card G)) . x = (h . x) + ((prime_factorization Gq) . x)

proof

let x be object ; :: thesis: ( x in SetPrimes implies (prime_factorization (card G)) . x = (h . x) + ((prime_factorization Gq) . x) )
assume x in SetPrimes ; :: thesis: (prime_factorization (card G)) . x = (h . x) + ((prime_factorization Gq) . x)

per cases ( not x in support (prime_factorization (card G)) or x in support (prime_factorization (card G)) ) ;

suppose A50: not x in support (prime_factorization (card G)) ; :: thesis: (prime_factorization (card G)) . x = (h . x) + ((prime_factorization Gq) . x)

then A51: not x in support h by A48;
A52: not x in support (prime_factorization Gq) by A32, A47, A50;
thus (prime_factorization (card G)) . x = 0 by PRE_POLY:def 7, A50
.= (h . x) + 0 by PRE_POLY:def 7, A51
.= (h . x) + ((prime_factorization Gq) . x) by PRE_POLY:def 7, A52 ; :: thesis: verum

end;

suppose A53: x in support (prime_factorization (card G)) ; :: thesis: (prime_factorization (card G)) . x = (h . x) + ((prime_factorization Gq) . x)

A54: x in support (pfexp (card G)) by A53, NAT_3:def 9;
thus (prime_factorization (card G)) . x = (h . x) + ((prime_factorization Gq) . x) :: thesis: verum

proof

per cases ( x in support h or x in {q} ) by A53, A49, XBOOLE_0:def 3;

suppose x in support h ; :: thesis: (prime_factorization (card G)) . x = (h . x) + ((prime_factorization Gq) . x)

then A55: ( x in support (prime_factorization (card G)) & not x in {q} ) by A41, XBOOLE_0:def 5;
x in support (pfexp (card G)) by A55, NAT_3:def 9;
then reconsider x0 = x as Prime by NAT_3:34;
A56: h . x0 = ((prime_factorization (card G)) . x0) -' ((prime_factorization Gq) . x0) by PRE_POLY:def 6;
(prime_factorization Gq) . x0 = 0 by A55, A32, PRE_POLY:def 7;
hence (prime_factorization (card G)) . x = (h . x) + ((prime_factorization Gq) . x) by A56, NAT_D:40; :: thesis: verum

end;

suppose x in {q} ; :: thesis: (prime_factorization (card G)) . x = (h . x) + ((prime_factorization Gq) . x)

then A57: x = q by TARSKI:def 1;
A58: h . x = ((prime_factorization (card G)) . q) -' ((prime_factorization Gq) . q) by A57, PRE_POLY:def 6;
(prime_factorization (card G)) . q = q |^ (q |-count (card G)) by A57, A54, NAT_3:def 9;
then h . x = ((prime_factorization (card G)) . q) - ((prime_factorization Gq) . q) by A58, XREAL_0:def 2, A31;
hence (prime_factorization (card G)) . x = (h . x) + ((prime_factorization Gq) . x) by A57; :: thesis: verum

end;

end;

end;

end;

end;

end;

then h + (prime_factorization Gq) = prime_factorization (card G) by PRE_POLY:33;
then A59: Product (prime_factorization (card G)) = (Product h) * (Product (prime_factorization Gq)) by A32, XBOOLE_1:79, A41, NAT_3:19;
( not Product h is zero & not Product (prime_factorization Gq) is zero ) by A59, NAT_3:61;
then consider H, K being finite strict Subgroup of G such that
A60: ( card H = Product h & card K = Product (prime_factorization Gq) & the carrier of H /\ the carrier of K = {(1_ G)} & ex F being Homomorphism of (product <*H,K*>),G st
( F is bijective & ( for a, b being Element of G st a in H & b in K holds
F . <*a,b*> = a * b ) ) ) by A26, A59, Th18, A46, A42, INT_7:12;
reconsider H = H, K = K as finite commutative Group ;
A61: support (prime_factorization (card H)) = support h by INT_7:16, INT_7:def 1, A43, A60;
card (support (prime_factorization (card H))) = card (support h) by INT_7:16, INT_7:def 1, A43, A60
.= (card (support (prime_factorization (card G)))) - (card {q}) by A41, A28, EULER_1:4
.= (n + 1) - 1 by A4, CARD_1:30
.= n ;
then consider I0 being non empty finite set , F0 being Group-like associative commutative multMagma-Family of I0, HFG0 being Homomorphism of (product F0),H such that
A62: ( I0 = support (prime_factorization (card H)) & ( for p being Element of I0 holds
( F0 . p is strict Subgroup of H & card (F0 . p) = (prime_factorization (card H)) . p ) ) & ( for p, q being Element of I0 st p <> q holds
the carrier of (F0 . p) /\ the carrier of (F0 . q) = {(1_ H)} ) & HFG0 is bijective & ( for x being I0 -defined the carrier of H -valued total Function st ( for p being Element of I0 holds x . p in F0 . p ) holds
( x in product F0 & HFG0 . x = Product x ) ) ) by A3, A25;
set I = I0 \/ {q};
reconsider I = I0 \/ {q} as non empty finite set ;
A63: Product (prime_factorization (card H)) = Product h by A60, NAT_3:61;
then A64: prime_factorization (card H) = h by A46, INT_7:15;
A65: I = support (prime_factorization (card G)) by A62, A49, A46, INT_7:15, A63;
set F = F0 +* (q .--> K);
A67: dom (F0 +* (q .--> K)) = (dom F0) \/ (dom (q .--> K)) by FUNCT_4:def 1
.= I0 \/ (dom (q .--> K)) by PARTFUN1:def 2
.= I0 \/ {q} ;
then reconsider F = F0 +* (q .--> K) as I -defined Function by RELAT_1:def 18;
reconsider F = F as ManySortedSet of I by PARTFUN1:def 2, A67;
reconsider F = F as multMagma-Family of I ;
A74: for x being Element of I holds
( F . x is strict Subgroup of G & card (F . x) = (prime_factorization (card G)) . x )

proof

let x be Element of I; :: thesis: ( F . x is strict Subgroup of G & card (F . x) = (prime_factorization (card G)) . x )
A75: x in dom F by A67;
A76: x in (dom F0) \/ (dom (q .--> K)) by A75, FUNCT_4:def 1;
A77: I0 = support h by INT_7:16, INT_7:def 1, A43, A60, A62
.= (support (prime_factorization (card G))) \ {q} by A33, TARSKI:2 ;

per cases ( x in I0 or x in {q} ) by XBOOLE_0:def 3;

suppose A78: x in I0 ; :: thesis: ( F . x is strict Subgroup of G & card (F . x) = (prime_factorization (card G)) . x )

then not x in dom (q .--> K) by A77, XBOOLE_0:def 5;
then A79: F . x = F0 . x by FUNCT_4:def 1, A76;
reconsider p = x as Element of I0 by A78;
A80: ( F0 . p is strict Subgroup of H & card (F0 . p) = (prime_factorization (card H)) . p ) by A62;
A81: ( x in support (prime_factorization (card G)) & not x in {q} ) by A41, XBOOLE_0:def 5, A61, A62, A78;
x in support (pfexp (card G)) by A81, NAT_3:def 9;
then reconsider x0 = x as Prime by NAT_3:34;
A82: h . x0 = ((prime_factorization (card G)) . x0) -' ((prime_factorization Gq) . x0) by PRE_POLY:def 6;
(prime_factorization Gq) . x0 = 0 by A81, A32, PRE_POLY:def 7;
hence ( F . x is strict Subgroup of G & card (F . x) = (prime_factorization (card G)) . x ) by A79, A80, GROUP_2:56, A64, A82, NAT_D:40; :: thesis: verum

end;

suppose A83: x in {q} ; :: thesis: ( F . x is strict Subgroup of G & card (F . x) = (prime_factorization (card G)) . x )

then A84: F . x = (q .--> K) . x by FUNCT_4:def 1, A76;
x in support (prime_factorization (card G)) by A83, A47;
then A85: x in support (pfexp (card G)) by NAT_3:def 9;
A86: x = q by TARSKI:def 1, A83;
card (F . x) = Product (prime_factorization Gq) by A60, A83, FUNCOP_1:7, A84
.= Gq by NAT_3:61
.= (prime_factorization (card G)) . x by A86, A85, NAT_3:def 9 ;
hence ( F . x is strict Subgroup of G & card (F . x) = (prime_factorization (card G)) . x ) by A84, A83, FUNCOP_1:7; :: thesis: verum

end;

end;

end;

A87: for i being Element of I holds F . i is Group-like by A74;
A88: for i being Element of I holds F . i is associative by A74;
for i being Element of I holds F . i is commutative by A74;
then reconsider F = F as Group-like associative commutative multMagma-Family of I by A87, GROUP_7:def 6, A88, GROUP_7:def 7, GROUP_7:def 8;
consider FHKG being Homomorphism of (product <*H,K*>),G such that
A89: ( FHKG is bijective & ( for a, b being Element of G st a in H & b in K holds
FHKG . <*a,b*> = a * b ) ) by A60;
A90: I0 = support h by INT_7:16, INT_7:def 1, A43, A60, A62
.= (support (prime_factorization (card G))) \ {q} by TARSKI:2, A33
.= I \ {q} by A62, A49, A46, INT_7:15, A63 ;
A91: not q in I0

proof

assume q in I0 ; :: thesis: contradiction
then ( q in I & not q in {q} ) by A90, XBOOLE_0:def 5;
hence contradiction by TARSKI:def 1; :: thesis: verum

end;

then consider FHK being Homomorphism of (product F),(product <*H,K*>) such that
A92: ( FHK is bijective & ( for x0 being Function
for k being Element of K
for h being Element of H st h = HFG0 . x0 & x0 in product F0 holds
FHK . (x0 +* (q .--> k)) = <*h,k*> ) ) by Th28, A62, A28, A65;
reconsider HFG = FHKG * FHK as Function of (product F),G ;
A93: HFG is onto by FUNCT_2:27, A89, A92;
reconsider HFG = HFG as Homomorphism of (product F),G ;
A94: 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 )

proof

let x be I -defined the carrier of G -valued total Function; :: thesis: ( ( for p being Element of I holds x . p in F . p ) implies ( x in product F & HFG . x = Product x ) )
assume A95: for p being Element of I holds x . p in F . p ; :: thesis: ( x in product F & HFG . x = Product x )
then x in the carrier of (product F) by Th29;
then consider x0 being I0 -defined total Function, k being Element of K such that
A96: ( x0 in product F0 & x = x0 +* (q .--> k) & ( for p being Element of I0 holds x0 . p in F0 . p ) ) by Th30, A91, A28, A65;
reconsider h = HFG0 . x0 as Element of H by FUNCT_2:5, A96;
reconsider hh = h, kk = k as Element of G by GROUP_2:42;

now :: thesis: for y being object st y in rng x0 holds
y in the carrier of H

let y be object ; :: thesis: ( y in rng x0 implies y in the carrier of H )
assume y in rng x0 ; :: thesis: y in the carrier of H
then consider z being object such that
A97: ( z in dom x0 & y = x0 . z ) by FUNCT_1:def 3;
reconsider z = z as Element of I0 by A97;
A98: x0 . z in F0 . z by A96;
F0 . z is strict Subgroup of H by A62;
hence y in the carrier of H by A97, STRUCT_0:def 5, A98, GROUP_2:40; :: thesis: verum

end;

then reconsider x0 = x0 as I0 -defined the carrier of H -valued total Function by RELAT_1:def 19, TARSKI:def 3;
A99: HFG0 . x0 = Product x0 by A62, A96;
the carrier of H c= the carrier of G by GROUP_2:def 5;
then rng x0 c= the carrier of G by XBOOLE_1:1;
then reconsider xx0 = x0 as I0 -defined the carrier of G -valued total Function by RELAT_1:def 19;
A100: Product x0 = Product xx0 by Th32;
thus x in product F by Th29, A95; :: thesis: HFG . x = Product x
A101: ( hh in H & kk in K ) ;
thus HFG . x = FHKG . (FHK . x) by FUNCT_2:15, Th29, A95
.= FHKG . <*hh,kk*> by A92, A96
.= hh * kk by A89, A101
.= Product x by A99, A100, Th33, A91, A28, A65, A96 ; :: thesis: verum

end;

for s, t being Element of I st s <> t holds
the carrier of (F . s) /\ the carrier of (F . t) = {(1_ G)}

proof

let s, t be Element of I; :: thesis: ( s <> t implies the carrier of (F . s) /\ the carrier of (F . t) = {(1_ G)} )
assume A102: s <> t ; :: thesis: the carrier of (F . s) /\ the carrier of (F . t) = {(1_ G)}
dom F = I by PARTFUN1:def 2;
then A103: ( s in dom F & t in dom F ) ;

per cases ( ( s in I0 & t in I0 ) or not s in I0 or not t in I0 ) ;

suppose ( s in I0 & t in I0 ) ; :: thesis: the carrier of (F . s) /\ the carrier of (F . t) = {(1_ G)}

then reconsider ss = s, tt = t as Element of I0 ;
A104: s in (dom F0) \/ (dom (q .--> K)) by A103, FUNCT_4:def 1;
A105: t in (dom F0) \/ (dom (q .--> K)) by A103, FUNCT_4:def 1;
A106: I0 = support h by INT_7:16, INT_7:def 1, A43, A60, A62
.= (support (prime_factorization (card G))) \ {q} by TARSKI:2, A33 ;
then not ss in dom (q .--> K) by XBOOLE_0:def 5;
then A107: F . ss = F0 . ss by FUNCT_4:def 1, A104;
not tt in dom (q .--> K) by A106, XBOOLE_0:def 5;
then A108: F . tt = F0 . tt by FUNCT_4:def 1, A105;
the carrier of (F0 . ss) /\ the carrier of (F0 . tt) = {(1_ H)} by A62, A102;
hence the carrier of (F . s) /\ the carrier of (F . t) = {(1_ G)} by A107, A108, GROUP_2:44; :: thesis: verum

end;

suppose A109: ( not s in I0 or not t in I0 ) ; :: thesis: the carrier of (F . s) /\ the carrier of (F . t) = {(1_ G)}

thus the carrier of (F . s) /\ the carrier of (F . t) = {(1_ G)} :: thesis: verum

proof

per cases ( not s in I0 or not t in I0 ) by A109;

suppose A110: not s in I0 ; :: thesis: the carrier of (F . s) /\ the carrier of (F . t) = {(1_ G)}

A111: s in (dom F0) \/ (dom (q .--> K)) by A103, FUNCT_4:def 1;
A112: s in {q} by A110, A90, XBOOLE_0:def 5;
then F . s = (q .--> K) . s by FUNCT_4:def 1, A111;
then A113: F . s = K by A112, FUNCOP_1:7;
t in I0

proof

assume not t in I0 ; :: thesis: contradiction
then ( not t in I or t in {q} ) by XBOOLE_0:def 5, A90;
then t = q by TARSKI:def 1;
hence contradiction by A102, TARSKI:def 1, A112; :: thesis: verum

end;

then reconsider tt = t as Element of I0 ;
A114: tt in (dom F0) \/ (dom (q .--> K)) by A103, FUNCT_4:def 1;
I0 = support h by INT_7:16, INT_7:def 1, A43, A60, A62
.= (support (prime_factorization (card G))) \ {q} by TARSKI:2, A33 ;
then not tt in dom (q .--> K) by XBOOLE_0:def 5;
then A115: F . tt = F0 . tt by FUNCT_4:def 1, A114;
reconsider S1 = F0 . tt as strict Subgroup of H by A62;
A116: the carrier of K /\ the carrier of S1 c= {(1_ G)} by A60, XBOOLE_1:26, GROUP_2:def 5;
A117: 1_ G in the carrier of K by GROUP_2:46, STRUCT_0:def 5;
1_ H in the carrier of S1 by GROUP_2:46, STRUCT_0:def 5;
then 1_ G in the carrier of S1 by GROUP_2:44;
then 1_ G in the carrier of K /\ the carrier of S1 by XBOOLE_0:def 4, A117;
then {(1_ G)} c= the carrier of K /\ the carrier of S1 by ZFMISC_1:31;
hence the carrier of (F . s) /\ the carrier of (F . t) = {(1_ G)} by A113, A115, A116, XBOOLE_0:def 10; :: thesis: verum

end;

suppose A118: not t in I0 ; :: thesis: the carrier of (F . s) /\ the carrier of (F . t) = {(1_ G)}

A119: t in (dom F0) \/ (dom (q .--> K)) by A103, FUNCT_4:def 1;
A120: t in {q} by A118, A90, XBOOLE_0:def 5;
then F . t = (q .--> K) . t by FUNCT_4:def 1, A119;
then A121: F . t = K by A120, FUNCOP_1:7;
s in I0

proof

assume not s in I0 ; :: thesis: contradiction
then ( not s in I or s in {q} ) by XBOOLE_0:def 5, A90;
then s = q by TARSKI:def 1;
hence contradiction by A102, TARSKI:def 1, A120; :: thesis: verum

end;

then reconsider ss = s as Element of I0 ;
A122: ss in (dom F0) \/ (dom (q .--> K)) by A103, FUNCT_4:def 1;
I0 = support h by INT_7:16, INT_7:def 1, A43, A60, A62
.= (support (prime_factorization (card G))) \ {q} by A33, TARSKI:2 ;
then not ss in dom (q .--> K) by XBOOLE_0:def 5;
then A123: F . ss = F0 . ss by FUNCT_4:def 1, A122;
reconsider S1 = F0 . ss as strict Subgroup of H by A62;
A124: the carrier of K /\ the carrier of S1 c= {(1_ G)} by A60, XBOOLE_1:26, GROUP_2:def 5;
A125: 1_ G in the carrier of K by GROUP_2:46, STRUCT_0:def 5;
1_ H in the carrier of S1 by GROUP_2:46, STRUCT_0:def 5;
then 1_ G in the carrier of S1 by GROUP_2:44;
then 1_ G in the carrier of K /\ the carrier of S1 by XBOOLE_0:def 4, A125;
then {(1_ G)} c= the carrier of K /\ the carrier of S1 by ZFMISC_1:31;
hence the carrier of (F . s) /\ the carrier of (F . t) = {(1_ G)} by A121, A123, A124, XBOOLE_0:def 10; :: thesis: verum

end;

end;

end;

end;

end;

end;

hence 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 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 A65, A74, A93, A89, A92, A94; :: thesis: verum

end;

end;

end;

end;

A126: for k being Nat holds S₁[k] from NAT_1:sch 2(A1, A2);
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 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 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 ) ) ) )
assume A127: card G > 1 ; :: thesis: 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 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 ) ) )
card (support (prime_factorization (card G))) <> 0

proof

assume card (support (prime_factorization (card G))) = 0 ; :: thesis: contradiction
then support (prime_factorization (card G)) = {} ;
hence contradiction by A127, NAT_3:57; :: thesis: verum

end;

hence 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 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 A126; :: thesis: verum