let G be finite commutative Group; :: thesis: for h, k being non zero Nat st card G = h * k & h,k are_coprime holds

ex H, K being finite strict Subgroup of G st

( card H = h & card K = k & 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 ) ) )

let h, k be non zero Nat; :: thesis: ( card G = h * k & h,k are_coprime implies ex H, K being finite strict Subgroup of G st

( card H = h & card K = k & 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 ) ) ) )

assume A1: ( card G = h * k & h,k are_coprime ) ; :: thesis: ex H, K being finite strict Subgroup of G st

( card H = h & card K = k & 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 ) ) )

then consider H, K being finite strict Subgroup of G such that

A2: ( the carrier of H = { x where x is Element of G : x |^ h = 1_ G } & the carrier of K = { x where x is Element of G : x |^ k = 1_ G } & H is normal & K is normal & ( for x being Element of G ex a, b being Element of G st

( a in H & b in K & x = a * b ) ) & the carrier of H /\ the carrier of K = {(1_ G)} ) by Th16;

take H ; :: thesis: ex K being finite strict Subgroup of G st

( card H = h & card K = k & 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 ) ) )

take K ; :: thesis: ( card H = h & card K = k & 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 ) ) )

consider F being Homomorphism of (product <*H,K*>),G such that

A3: ( F is bijective & ( for a, b being Element of G st a in H & b in K holds

F . <*a,b*> = a * b ) ) by A2, Th12;

set s = card H;

set t = card K;

( F is one-to-one & dom F = the carrier of (product <*H,K*>) & rng F = the carrier of G ) by A3, FUNCT_2:def 1, FUNCT_2:def 3;

then card (product <*H,K*>) = card G by CARD_1:5, WELLORD2:def 4;

then A4: (card H) * (card K) = h * k by A1, Th17;

A5: for q being Prime st q in support (prime_factorization (card H)) holds

not q,h are_coprime by A2, Th15;

for q being Prime st q in support (prime_factorization (card K)) holds

not q,k are_coprime by A2, Th15;

hence ( card H = h & card K = k & 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 A2, A3, A4, Th7, A5, A1; :: thesis: verum

ex H, K being finite strict Subgroup of G st

( card H = h & card K = k & 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 ) ) )

let h, k be non zero Nat; :: thesis: ( card G = h * k & h,k are_coprime implies ex H, K being finite strict Subgroup of G st

( card H = h & card K = k & 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 ) ) ) )

assume A1: ( card G = h * k & h,k are_coprime ) ; :: thesis: ex H, K being finite strict Subgroup of G st

( card H = h & card K = k & 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 ) ) )

then consider H, K being finite strict Subgroup of G such that

A2: ( the carrier of H = { x where x is Element of G : x |^ h = 1_ G } & the carrier of K = { x where x is Element of G : x |^ k = 1_ G } & H is normal & K is normal & ( for x being Element of G ex a, b being Element of G st

( a in H & b in K & x = a * b ) ) & the carrier of H /\ the carrier of K = {(1_ G)} ) by Th16;

take H ; :: thesis: ex K being finite strict Subgroup of G st

( card H = h & card K = k & 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 ) ) )

take K ; :: thesis: ( card H = h & card K = k & 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 ) ) )

consider F being Homomorphism of (product <*H,K*>),G such that

A3: ( F is bijective & ( for a, b being Element of G st a in H & b in K holds

F . <*a,b*> = a * b ) ) by A2, Th12;

set s = card H;

set t = card K;

( F is one-to-one & dom F = the carrier of (product <*H,K*>) & rng F = the carrier of G ) by A3, FUNCT_2:def 1, FUNCT_2:def 3;

then card (product <*H,K*>) = card G by CARD_1:5, WELLORD2:def 4;

then A4: (card H) * (card K) = h * k by A1, Th17;

A5: for q being Prime st q in support (prime_factorization (card H)) holds

not q,h are_coprime by A2, Th15;

for q being Prime st q in support (prime_factorization (card K)) holds

not q,k are_coprime by A2, Th15;

hence ( card H = h & card K = k & 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 A2, A3, A4, Th7, A5, A1; :: thesis: verum