let G be 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 ( multMagma(# the carrier of G, the multF of G #) = gr (Union (Carrier F)) & ( 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 ) ) )
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 ( multMagma(# the carrier of G, the multF of G #) = gr (Union (Carrier F)) & ( 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 ) ) )
let F be normal Subgroup-Family of I,G; :: thesis: ( F is one-to-one implies ( G is_internal_product_of F iff ( multMagma(# the carrier of G, the multF of G #) = gr (Union (Carrier F)) & ( 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 ) ) ) )
assume A1: F is one-to-one ; :: thesis: ( G is_internal_product_of F iff ( multMagma(# the carrier of G, the multF of G #) = gr (Union (Carrier F)) & ( 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 ) ) )
thus ( G is_internal_product_of F implies ( multMagma(# the carrier of G, the multF of G #) = gr (Union (Carrier F)) & ( 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 ) ) ) :: thesis: ( multMagma(# the carrier of G, the multF of G #) = gr (Union (Carrier F)) & ( 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 ) implies G is_internal_product_of F )

proof

assume Z2: G is_internal_product_of F ; :: thesis: ( multMagma(# the carrier of G, the multF of G #) = gr (Union (Carrier F)) & ( 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 ) )
hence multMagma(# the carrier of G, the multF of G #) = gr (Union (Carrier F)) ; :: thesis: 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
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
A2: {i} c= { j where j is Element of I : F . i = F . j }

proof

for x being object st x in {i} holds
x in { j where j is Element of I : F . i = F . j }

proof

let x be object ; :: thesis: ( x in {i} implies x in { j where j is Element of I : F . i = F . j } )
assume x in {i} ; :: thesis: x in { j where j is Element of I : F . i = F . j }
then x = i by TARSKI:def 1;
hence x in { j where j is Element of I : F . i = F . j } ; :: thesis: verum

end;

hence {i} c= { j where j is Element of I : F . i = F . j } by TARSKI:def 3; :: thesis: verum

end;

for x being object st x in { j where j is Element of I : F . i = F . j } holds
x in {i}

proof

let x be object ; :: thesis: ( x in { j where j is Element of I : F . i = F . j } implies x in {i} )
assume x in { j where j is Element of I : F . i = F . j } ; :: thesis: x in {i}
then consider j being Element of I such that
B2: ( x = j & F . i = F . j ) ;
dom F = I by PARTFUN1:def 2;
then i = j by A1, B2;
hence x in {i} by B2, TARSKI:def 1; :: thesis: verum

end;

then A3: { j where j is Element of I : F . i = F . j } c= {i} by TARSKI:def 3;
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 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
then Z4: J = I \ { j where j is Element of I : F . i = F . j } by A2, A3, XBOOLE_0:def 10;
let N be strict normal Subgroup of G; :: thesis: ( N = gr (Union (Carrier (F | J))) implies (F . i) /\ N = (1). G )
assume N = gr (Union (Carrier (F | J))) ; :: thesis: (F . i) /\ N = (1). G
hence (F . i) /\ N = (1). G by Z2, Z4, ThIPO; :: thesis: verum

end;

assume Z6: multMagma(# the carrier of G, the multF of G #) = gr (Union (Carrier F)) ; :: thesis: ( ex i being Element of I ex J being Subset of I st
( J = I \ {i} & ex N being strict normal Subgroup of G st
( N = gr (Union (Carrier (F | J))) & not (F . i) /\ N = (1). G ) ) or G is_internal_product_of F )
assume Z7: 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 ; :: thesis: G is_internal_product_of F
for i being Element of I
for J being Subset of I st J = I \ { j where j is Element of I : F . i = F . j } 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 \ { j where j is Element of I : F . i = F . j } 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 \ { j where j is Element of I : F . i = F . j } 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 \ { j where j is Element of I : F . i = F . j } ; :: thesis: for N being strict normal Subgroup of G st N = gr (Union (Carrier (F | J))) holds
(F . i) /\ N = (1). G
A2: {i} c= { j where j is Element of I : F . i = F . j }

proof

for x being object st x in {i} holds
x in { j where j is Element of I : F . i = F . j }

proof

let x be object ; :: thesis: ( x in {i} implies x in { j where j is Element of I : F . i = F . j } )
assume x in {i} ; :: thesis: x in { j where j is Element of I : F . i = F . j }
then x = i by TARSKI:def 1;
hence x in { j where j is Element of I : F . i = F . j } ; :: thesis: verum

end;

hence {i} c= { j where j is Element of I : F . i = F . j } by TARSKI:def 3; :: thesis: verum

end;

for x being object st x in { j where j is Element of I : F . i = F . j } holds
x in {i}

proof

let x be object ; :: thesis: ( x in { j where j is Element of I : F . i = F . j } implies x in {i} )
assume x in { j where j is Element of I : F . i = F . j } ; :: thesis: x in {i}
then consider j being Element of I such that
B1: ( x = j & F . i = F . j ) ;
dom F = I by PARTFUN1:def 2;
then i = j by A1, B1;
hence x in {i} by B1, TARSKI:def 1; :: thesis: verum

end;

then { j where j is Element of I : F . i = F . j } c= {i} by TARSKI:def 3;
then A3: { j where j is Element of I : F . i = F . j } = {i} by A2, XBOOLE_0:def 10;
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
thus (F . i) /\ N = (1). G by Z7, B2, B3, A3; :: thesis: verum

end;

hence G is_internal_product_of F by Z6, ThIPO; :: thesis: verum