defpred S_{1}[ 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_{2} -defined the carrier of b_{1} -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_{1}[ 0 ]
;

A2: for n being Nat st S_{1}[n] holds

S_{1}[n + 1]
_{1}[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_{1} -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_{1} -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

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

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

( x in product F & HFG . x = Product x ) ) );

A1: S

A2: for n being Nat st S

S

proof

A126:
for k being Nat holds S
let n be Nat; :: thesis: ( S_{1}[n] implies S_{1}[n + 1] )

assume A3: S_{1}[n]
; :: thesis: S_{1}[n + 1]

thus S_{1}[n + 1]
:: thesis: verum

end;assume A3: S

thus S

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

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

( 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

( x in product F & HFG . x = Product x ) ) )

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

end;

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

( 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

( 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

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))

.= card G by NAT_3:61 ;

reconsider I = {q} as non empty finite set ;

set F = q .--> G;

for y being set st y in rng (q .--> G) holds

y is non empty multMagma

A16: for s, t being Element of I st s <> t holds

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

( F . x is strict Subgroup of G & card (F . x) = (prime_factorization (card G)) . x )

A23: for i being Element of I holds F . i is associative ;

for i being Element of I holds F . i is commutative ;

then reconsider F = F as Group-like associative commutative multMagma-Family of I by A22, GROUP_7:def 6, A23, GROUP_7:def 7, GROUP_7:def 8;

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

then A11:
support (pfexp Gq) = {q}
by NAT_3:42;
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 (prime_factorization (card G)) . q = 0 by NAT_3:55;

hence contradiction by A7, PRE_POLY:def 7; :: thesis: verum

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

then A14: Gq =
Product (prime_factorization (card G))
by A13, NAT_3:def 9, A10
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;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

.= card G by NAT_3:61 ;

reconsider I = {q} as non empty finite set ;

set F = q .--> G;

for y being set st y in rng (q .--> G) holds

y is non empty multMagma

proof

then reconsider F = q .--> G as multMagma-Family of I by GROUP_7:def 1;
let y be set ; :: thesis: ( y in rng (q .--> G) implies y is non empty multMagma )

assume y in rng (q .--> G) ; :: thesis: y is non empty multMagma

then consider x being object such that

A15: ( x in dom (q .--> G) & y = (q .--> G) . x ) by FUNCT_1:def 3;

thus y is non empty multMagma by FUNCOP_1:7, A15; :: thesis: verum

end;assume y in rng (q .--> G) ; :: thesis: y is non empty multMagma

then consider x being object such that

A15: ( x in dom (q .--> G) & y = (q .--> G) . x ) by FUNCT_1:def 3;

thus y is non empty multMagma by FUNCOP_1:7, A15; :: thesis: verum

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

A18:
for x being Element of I holds
let s, t be Element of I; :: thesis: ( s <> t implies the carrier of (F . s) /\ the carrier of (F . t) = {(1_ G)} )

assume A17: s <> t ; :: thesis: the carrier of (F . s) /\ the carrier of (F . t) = {(1_ G)}

s = q by TARSKI:def 1;

hence the carrier of (F . s) /\ the carrier of (F . t) = {(1_ G)} by A17, TARSKI:def 1; :: thesis: verum

end;assume A17: s <> t ; :: thesis: the carrier of (F . s) /\ the carrier of (F . t) = {(1_ G)}

s = q by TARSKI:def 1;

hence the carrier of (F . s) /\ the carrier of (F . t) = {(1_ G)} by A17, TARSKI:def 1; :: thesis: verum

( F . x is strict Subgroup of G & card (F . x) = (prime_factorization (card G)) . x )

proof

A22:
for i being Element of I holds F . i is Group-like
;
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;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

A23: for i being Element of I holds F . i is associative ;

for i being Element of I holds F . i is commutative ;

then reconsider F = F as Group-like associative commutative multMagma-Family of I by A22, GROUP_7:def 6, A23, GROUP_7:def 7, GROUP_7:def 8;

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

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

( 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

( 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

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} )

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 )

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)

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;

for y being set st y in rng F holds

y is non empty multMagma

A74: for x being Element of I holds

( F . x is strict Subgroup of G & card (F . x) = (prime_factorization (card G)) . x )

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

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 )

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

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

then A29:
support (pfexp Gq) = {q}
by NAT_3:42;
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 (prime_factorization (card G)) . q = 0 by NAT_3:55;

hence contradiction by A28, PRE_POLY:def 7; :: thesis: verum

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

then A41:
support ((prime_factorization (card G)) -' (prime_factorization Gq)) = (support (prime_factorization (card G))) \ {q}
by TARSKI:2;
let x be object ; :: thesis: ( x in support ((prime_factorization (card G)) -' (prime_factorization Gq)) iff x in (support (prime_factorization (card G))) \ {q} )

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;hereby :: thesis: ( x in (support (prime_factorization (card G))) \ {q} implies x in support ((prime_factorization (card G)) -' (prime_factorization Gq)) )

assume
x in (support (prime_factorization (card G))) \ {q}
; :: thesis: 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}

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

hence
x in (support (prime_factorization (card G))) \ {q}
by XBOOLE_0:def 5, A35; :: thesis: verum
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;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

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

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

then A46:
h is prime-factorization-like
by INT_7:def 1;
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;( 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

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

then
h + (prime_factorization Gq) = prime_factorization (card G)
by PRE_POLY:33;
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)

end;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)) )
;

end;

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

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

end;thus (prime_factorization (card G)) . x = (h . x) + ((prime_factorization Gq) . x) :: thesis: verum

proof
end;

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

end;

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

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

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;

for y being set st y in rng F holds

y is non empty multMagma

proof

then reconsider F = F as multMagma-Family of I by GROUP_7:def 1;
let y be set ; :: thesis: ( y in rng F implies y is non empty multMagma )

assume y in rng F ; :: thesis: y is non empty multMagma

then consider x being object such that

A68: ( x in dom F & y = F . x ) by FUNCT_1:def 3;

A69: x in (dom F0) \/ (dom (q .--> K)) by A68, FUNCT_4:def 1;

A70: I0 = support h by INT_7:16, INT_7:def 1, A43, A60, A62

.= (support (prime_factorization (card G))) \ {q} by TARSKI:2, A33 ;

end;assume y in rng F ; :: thesis: y is non empty multMagma

then consider x being object such that

A68: ( x in dom F & y = F . x ) by FUNCT_1:def 3;

A69: x in (dom F0) \/ (dom (q .--> K)) by A68, FUNCT_4:def 1;

A70: I0 = support h by INT_7:16, INT_7:def 1, A43, A60, A62

.= (support (prime_factorization (card G))) \ {q} by TARSKI:2, A33 ;

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

end;

suppose A71:
x in I0
; :: thesis: y is non empty multMagma

then
not x in dom (q .--> K)
by A70, XBOOLE_0:def 5;

then A72: F . x = F0 . x by FUNCT_4:def 1, A69;

x in dom F0 by A71, PARTFUN1:def 2;

then F0 . x in rng F0 by FUNCT_1:3;

hence y is non empty multMagma by A72, A68, GROUP_7:def 1; :: thesis: verum

end;then A72: F . x = F0 . x by FUNCT_4:def 1, A69;

x in dom F0 by A71, PARTFUN1:def 2;

then F0 . x in rng F0 by FUNCT_1:3;

hence y is non empty multMagma by A72, A68, GROUP_7:def 1; :: thesis: verum

A74: for x being Element of I holds

( F . x is strict Subgroup of G & card (F . x) = (prime_factorization (card G)) . x )

proof

A87:
for i being Element of I holds F . i is Group-like
by A74;
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 ;

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

end;

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

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

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

then consider FHK being Homomorphism of (product F),(product <*H,K*>) such that
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 ( q in I & not q in {q} ) by A90, XBOOLE_0:def 5;

hence contradiction by TARSKI:def 1; :: thesis: verum

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

for s, t being Element of I st s <> t holds
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;

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

then reconsider x0 = x0 as I0 -defined the carrier of H -valued total Function by RELAT_1:def 19, TARSKI:def 3;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;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

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

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

proof

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

end;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 )
;

end;

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

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

end;proof
end;

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

end;

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

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

then reconsider tt = t as Element of I0 ;
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 ( 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

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

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

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

then reconsider ss = s as Element of I0 ;
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 ( 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

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

( 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

( x in product F & HFG . x = Product x ) ) ) by A65, A74, A93, A89, A92, A94; :: thesis: verum

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

( 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

( x in product F & HFG . x = Product x ) ) )

card (support (prime_factorization (card G))) <> 0

proof

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
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;then support (prime_factorization (card G)) = {} ;

hence contradiction by A127, NAT_3:57; :: 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)} ) & HFG is bijective & ( for x being b

( x in product F & HFG . x = Product x ) ) ) by A126; :: thesis: verum