consider i being object such that
A1: i in I by XBOOLE_0:def 1;
consider F being Group-Family of I, h being Homomorphism of (sum F),((Omega). G) such that
A2: ( h is bijective & F = (I --> ((1). ((Omega). G))) +* ({i} --> ((Omega). G)) & ( for j being Element of I holds 1_ (F . j) = 1_ ((Omega). G) ) & ( for x being Element of (sum F) holds h . x = x . i ) & ( for x being Element of (sum F) ex J being finite Subset of I ex a being ManySortedSet of J st
( J c= {i} & J = support (x,F) & ( support (x,F) = {} or support (x,F) = {i} ) & x = (1_ (product F)) +* a & ( for j being Element of I st j in I \ J holds
x . j = 1_ (F . j) ) & ( for j being object st j in J holds
x . j = a . j ) ) ) ) by A1, Th43;
reconsider W = F . i as Group by A1, Th1;
reconsider h = h as Homomorphism of (sum F),G by Th6;
h is bijective by A2;
then reconsider F = F as DirectSumComponents of G,I by Def8;
set v = I --> ((1). ((Omega). G));
set w = {i} --> ((Omega). G);
A8: dom F = (dom (I --> ((1). ((Omega). G)))) \/ (dom ({i} --> ((Omega). G))) by A2, FUNCT_4:def 1
.= (dom (I --> ((1). ((Omega). G)))) \/ {i} by FUNCOP_1:13
.= I \/ {i} by FUNCOP_1:13
.= I by A1, XBOOLE_1:12, ZFMISC_1:31 ;
A9: i in {i} by TARSKI:def 1;
then i in dom ({i} --> ((Omega). G)) by FUNCOP_1:13;
then A11: F . i = ({i} --> ((Omega). G)) . i by A2, FUNCT_4:13;
then A12: F . i = (Omega). G by A9, FUNCOP_1:7;
A13: for j being object st j in I \ {i} holds
F . j = (1). ((Omega). G)
proof
let j be object ; :: thesis: ( j in I \ {i} implies F . j = (1). ((Omega). G) )
assume A14: j in I \ {i} ; :: thesis: F . j = (1). ((Omega). G)
then j in dom F by A8;
then A15: j in (dom (I --> ((1). ((Omega). G)))) \/ (dom ({i} --> ((Omega). G))) by A2, FUNCT_4:def 1;
not j in dom ({i} --> ((Omega). G)) by A14, XBOOLE_0:def 5;
hence F . j = (I --> ((1). ((Omega). G))) . j by A2, A15, FUNCT_4:def 1
.= (1). ((Omega). G) by A14, FUNCOP_1:7 ;
:: thesis: verum
end;
A21: for j being object st j in I holds
F . j is Subgroup of G
proof
let j be object ; :: thesis: ( j in I implies F . j is Subgroup of G )
assume A22: j in I ; :: thesis: F . j is Subgroup of G
then reconsider Z = F . j as Group by Th1;
per cases ( j in {i} or not j in {i} ) ;
suppose j in {i} ; :: thesis: F . j is Subgroup of G
hence F . j is Subgroup of G by A12, TARSKI:def 1; :: thesis: verum
end;
end;
end;
for x being finite-support Function of I,G st x in sum F holds
h . x = Product x
proof
let x be finite-support Function of I,G; :: thesis: ( x in sum F implies h . x = Product x )
assume A23: x in sum F ; :: thesis: h . x = Product x
then reconsider x0 = x as Element of (sum F) ;
set p = x | (support x);
A24: dom (x | (support x)) = support x by FUNCT_2:def 1;
A28: x0 in product F by A23, GROUP_2:40;
then A29: support (x0,F) = support x by A21, Th9;
A30: h . x0 = x0 . i by A2;
consider J being finite Subset of I, a being ManySortedSet of J such that
A31: ( J c= {i} & J = support (x0,F) & ( support (x0,F) = {} or support (x0,F) = {i} ) & x0 = (1_ (product F)) +* a & ( for j being Element of I st j in I \ J holds
x0 . j = 1_ (F . j) ) & ( for j being object st j in J holds
x0 . j = a . j ) ) by A2;
per cases ( support (x0,F) = {} or support (x0,F) = {i} ) by A31;
suppose A32: support (x0,F) = {} ; :: thesis: h . x = Product x
A34: x . i = 1_ W by A1, A31, A32
.= 1_ ((Omega). G) by A9, A11, FUNCOP_1:7 ;
(x | (support x)) * (canFS (support x)) = <*> the carrier of G by A29, A32;
then Product (x | (support x)) = Product (<*> the carrier of G) by GROUP_17:def 1
.= 1_ G by GROUP_4:8 ;
hence h . x = Product x by A30, A34, GROUP_2:44; :: thesis: verum
end;
suppose A36: support (x0,F) = {i} ; :: thesis: h . x = Product x
reconsider xi = x0 . i as Element of G by A30, FUNCT_2:5;
A37: i in dom (x | (support x)) by A24, A29, A36, TARSKI:def 1;
(x | (support x)) * (canFS (support x)) = (x | (support x)) * (canFS {i}) by A21, A28, A36, Th9
.= (x | (support x)) * <*i*> by FINSEQ_1:94
.= <*((x | (support x)) . i)*> by A37, FINSEQ_2:34
.= <*xi*> by A37, FUNCT_1:47 ;
then Product (x | (support x)) = Product <*xi*> by GROUP_17:def 1
.= x0 . i by GROUP_4:9 ;
hence h . x = Product x by A2; :: thesis: verum
end;
end;
end;
then F is internal by A2, A21;
hence ex b1 being DirectSumComponents of G,I st b1 is internal ; :: thesis: verum