let G be strict Group; :: thesis: for I being non empty set
for F being normal Subgroup-Family of I,G st F is one-to-one holds
( G is_internal_product_of F iff F is internal DirectSumComponents of G,I )
let I be non empty set ; :: thesis: for F being normal Subgroup-Family of I,G st F is one-to-one holds
( G is_internal_product_of F iff F is internal DirectSumComponents of G,I )
let F be normal Subgroup-Family of I,G; :: thesis: ( F is one-to-one implies ( G is_internal_product_of F iff F is internal DirectSumComponents of G,I ) )
assume A1: F is one-to-one ; :: thesis: ( G is_internal_product_of F iff F is internal DirectSumComponents of G,I )
A2: for i being Element of I
for J being Subset of I holds Carrier (F | J) = (Carrier F) | J

proof

let i be Element of I; :: thesis: for J being Subset of I holds Carrier (F | J) = (Carrier F) | J
let J be Subset of I; :: thesis: Carrier (F | J) = (Carrier F) | J

per cases ( J is empty or not J is empty ) ;

suppose J is empty ; :: thesis: Carrier (F | J) = (Carrier F) | J

hence Carrier (F | J) = (Carrier F) | J ; :: thesis: verum

end;

suppose not J is empty ; :: thesis: Carrier (F | J) = (Carrier F) | J

then reconsider J = J as non empty Subset of I ;
for j being Element of J holds (Carrier (F | J)) . j = ((Carrier F) | J) . j

proof

let j be Element of J; :: thesis: (Carrier (F | J)) . j = ((Carrier F) | J) . j
j in J ;
then j in dom (F | J) by PARTFUN1:def 2;
then B1: (F | J) . j = F . j by FUNCT_1:47;
B2: (Carrier (F | J)) . j = the carrier of (F . j) by B1, Th9
.= (Carrier F) . j by Th9 ;
dom ((Carrier F) | J) = J by PARTFUN1:def 2;
hence (Carrier (F | J)) . j = ((Carrier F) | J) . j by B2, FUNCT_1:47; :: thesis: verum

end;

hence Carrier (F | J) = (Carrier F) | J by PBOOLE:def 21; :: thesis: verum

end;

end;

end;

thus ( G is_internal_product_of F implies F is internal DirectSumComponents of G,I ) :: thesis: ( F is internal DirectSumComponents of G,I implies G is_internal_product_of F )

proof

assume A3: G is_internal_product_of F ; :: thesis: F is internal DirectSumComponents of G,I
A4: for i being Element of I holds F . i is normal Subgroup of G ;
A6: for i being Element of I ex UFi being Subset of G st
( UFi = Union ((Carrier F) | (I \ {i})) & ([#] (gr UFi)) /\ ([#] (F . i)) = {(1_ G)} )

proof

let i be Element of I; :: thesis: ex UFi being Subset of G st
( UFi = Union ((Carrier F) | (I \ {i})) & ([#] (gr UFi)) /\ ([#] (F . i)) = {(1_ G)} )
set J = I \ {i};
take UFi = Union (Carrier (F | (I \ {i}))); :: thesis: ( UFi = Union ((Carrier F) | (I \ {i})) & ([#] (gr UFi)) /\ ([#] (F . i)) = {(1_ G)} )
thus UFi = Union ((Carrier F) | (I \ {i})) by A2; :: thesis: ([#] (gr UFi)) /\ ([#] (F . i)) = {(1_ G)}
consider N being strict normal Subgroup of G such that
B3: N = gr (Union (Carrier (F | (I \ {i})))) by ThJoinNormUnionRes;
B4: (F . i) /\ N = (1). G by A1, A3, B3, ThInjectiveIPO;
[#] ((F . i) /\ N) = (carr (F . i)) /\ (carr N) by GROUP_2:def 10
.= ([#] (F . i)) /\ ([#] (gr UFi)) by B3 ;
hence ([#] (gr UFi)) /\ ([#] (F . i)) = {(1_ G)} by B4, GROUP_2:def 7; :: thesis: verum

end;

thus F is internal DirectSumComponents of G,I by A3, A4, A6, GROUP_20:16; :: thesis: verum

end;

thus ( F is internal DirectSumComponents of G,I implies G is_internal_product_of F ) :: thesis: verum

proof

assume A3: F is internal DirectSumComponents of G,I ; :: thesis: G is_internal_product_of F
A5: ex UF being Subset of G st
( UF = Union (Carrier F) & gr UF = G ) by A3, GROUP_20:16;
for i being Element of I
for J being Subset of I st J = I \ {i} holds
for N being strict normal Subgroup of G st N = gr (Union (Carrier (F | J))) holds
(F . i) /\ N = (1). G

proof

let i be Element of I; :: thesis: for J being Subset of I st J = I \ {i} holds
for N being strict normal Subgroup of G st N = gr (Union (Carrier (F | J))) holds
(F . i) /\ N = (1). G
let J be Subset of I; :: thesis: ( J = I \ {i} implies for N being strict normal Subgroup of G st N = gr (Union (Carrier (F | J))) holds
(F . i) /\ N = (1). G )
assume B2: J = I \ {i} ; :: thesis: for N being strict normal Subgroup of G st N = gr (Union (Carrier (F | J))) holds
(F . i) /\ N = (1). G
let N be strict normal Subgroup of G; :: thesis: ( N = gr (Union (Carrier (F | J))) implies (F . i) /\ N = (1). G )
assume B3: N = gr (Union (Carrier (F | J))) ; :: thesis: (F . i) /\ N = (1). G
consider UFi being Subset of G such that
B4: UFi = Union ((Carrier F) | (I \ {i})) and
B5: ([#] (gr UFi)) /\ ([#] (F . i)) = {(1_ G)} by A3, GROUP_20:16;
N = gr UFi by A2, B2, B3, B4;
then B6: ([#] N) /\ ([#] (F . i)) = carr ((1). G) by B5, GROUP_2:def 7;
reconsider Fi = F . i as Subgroup of G ;
carr (N /\ Fi) = (carr N) /\ (carr Fi) by GROUP_2:81;
hence (F . i) /\ N = (1). G by B6, GROUP_2:59; :: thesis: verum

end;

hence G is_internal_product_of F by A1, A5, ThInjectiveIPO; :: thesis: verum

end;