let I be non empty set ; :: thesis: for G being Group
for M being DirectSumComponents of G,I ex f being Homomorphism of (sum M),G ex N being internal DirectSumComponents of G,I st
( f is bijective & ( for i being Element of I ex qi being Homomorphism of (M . i),(N . i) st
( qi = f * (1ProdHom (M,i)) & qi is bijective ) ) )

let G be Group; :: thesis: for M being DirectSumComponents of G,I ex f being Homomorphism of (sum M),G ex N being internal DirectSumComponents of G,I st
( f is bijective & ( for i being Element of I ex qi being Homomorphism of (M . i),(N . i) st
( qi = f * (1ProdHom (M,i)) & qi is bijective ) ) )

let M be DirectSumComponents of G,I; :: thesis: ex f being Homomorphism of (sum M),G ex N being internal DirectSumComponents of G,I st
( f is bijective & ( for i being Element of I ex qi being Homomorphism of (M . i),(N . i) st
( qi = f * (1ProdHom (M,i)) & qi is bijective ) ) )

consider f being Homomorphism of (sum M),G such that
A1: f is bijective by GROUP_19:def 8;
deffunc H1( Element of I) -> Subgroup of G = f .: (ProjGroup (M,\$1));
consider N being Function such that
A2: dom N = I and
A3: for i being Element of I st i in I holds
N . i = H1(i) from A4: for i being object st i in I holds
N . i is strict Subgroup of G
proof
let i be object ; :: thesis: ( i in I implies N . i is strict Subgroup of G )
assume i in I ; :: thesis: N . i is strict Subgroup of G
then reconsider i = i as Element of I ;
N . i = f .: (ProjGroup (M,i)) by A3;
hence N . i is strict Subgroup of G ; :: thesis: verum
end;
then for i being object st i in I holds
N . i is Group ;
then reconsider N = N as Group-Family of I by ;
for i being object st i in I holds
N . i is Subgroup of G by A4;
then reconsider N = N as Subgroup-Family of I,G by Def1;
A5: for i being Element of I holds N . i is Subgroup of G by A4;
deffunc H2( Element of I) -> Element of K19(K20( the carrier of (M . \$1), the carrier of G)) = f * (1ProdHom (M,\$1));
consider q being Function such that
A6: dom q = I and
A7: for i being Element of I st i in I holds
q . i = H2(i) from reconsider q = q as non empty Function by A6;
A8: now :: thesis: for i being Element of I ex qi being Homomorphism of (M . i),(N . i) st
( qi = q . i & qi is bijective )
let i be Element of I; :: thesis: ex qi being Homomorphism of (M . i),(N . i) st
( qi = q . i & qi is bijective )

A9: rng (1ProdHom (M,i)) = [#] (ProjGroup (M,i)) by FUNCT_2:def 3;
reconsider fi = f | (ProjGroup (M,i)) as Homomorphism of (ProjGroup (M,i)),G ;
dom fi = [#] (ProjGroup (M,i)) by FUNCT_2:def 1;
then A10: f * (1ProdHom (M,i)) = fi * (1ProdHom (M,i)) by ;
A11: rng fi = f .: ([#] (ProjGroup (M,i))) by RELAT_1:115
.= [#] (f .: (ProjGroup (M,i))) by GRSOLV_1:8
.= [#] (N . i) by A3 ;
Image fi = f .: (ProjGroup (M,i))
.= N . i by A3 ;
then reconsider fi = fi as Homomorphism of (ProjGroup (M,i)),(N . i) by GROUP_6:49;
A12: fi is one-to-one by ;
A13: fi is onto by ;
reconsider qi = fi * (1ProdHom (M,i)) as Homomorphism of (M . i),(N . i) ;
take qi = qi; :: thesis: ( qi = q . i & qi is bijective )
thus qi = q . i by ; :: thesis: qi is bijective
thus qi is bijective by ; :: thesis: verum
end;
then A14: for i being Element of I ex qi being Homomorphism of (M . i),(N . i) st
( qi = q . i & qi is bijective ) ;
reconsider r = SumMap (M,N,q) as Homomorphism of (sum M),(sum N) ;
A15: r is bijective by ;
reconsider s = r " as Homomorphism of (sum N),(sum M) by ;
A16: s is bijective by ;
reconsider g = f * s as Function ;
reconsider g = g as Homomorphism of (sum N),G ;
A17: g is bijective by ;
then reconsider N = N as DirectSumComponents of G,I by GROUP_19:def 8;
for i being Element of I
for n being Element of (N . i) holds g . ((1ProdHom (N,i)) . n) = n
proof
let i be Element of I; :: thesis: for n being Element of (N . i) holds g . ((1ProdHom (N,i)) . n) = n
let n be Element of (N . i); :: thesis: g . ((1ProdHom (N,i)) . n) = n
consider qi being Homomorphism of (M . i),(N . i) such that
A18: qi = q . i and
A19: qi is bijective by A8;
A20: dom qi = [#] (M . i) by FUNCT_2:def 1;
rng qi = [#] (N . i) by ;
then consider m being object such that
A21: m in [#] (M . i) and
A22: qi . m = n by ;
reconsider m = m as Element of (M . i) by A21;
for i being Element of I holds q . i is Homomorphism of (M . i),(N . i)
proof
let i be Element of I; :: thesis: q . i is Homomorphism of (M . i),(N . i)
ex qi being Homomorphism of (M . i),(N . i) st
( qi = q . i & qi is bijective ) by A8;
hence q . i is Homomorphism of (M . i),(N . i) ; :: thesis: verum
end;
then A24: r . ((1ProdHom (M,i)) . m) = (1ProdHom (N,i)) . n by ;
A25: dom r = [#] (sum M) by FUNCT_2:def 1;
(1ProdHom (M,i)) . m in ProjGroup (M,i) ;
then A26: (1ProdHom (M,i)) . m in sum M by GROUP_2:40;
A27: dom s = [#] (sum N) by FUNCT_2:def 1;
(1ProdHom (N,i)) . n in ProjGroup (N,i) ;
then A28: (1ProdHom (N,i)) . n in sum N by GROUP_2:40;
A29: qi = f * (1ProdHom (M,i)) by ;
A30: m in dom (1ProdHom (M,i)) by ;
g . ((1ProdHom (N,i)) . n) = f . (s . ((1ProdHom (N,i)) . n)) by
.= f . ((1ProdHom (M,i)) . m) by
.= n by ;
hence g . ((1ProdHom (N,i)) . n) = n ; :: thesis: verum
end;
then for a being finite-support Function of I,G st a in sum N holds
g . a = Product a by Th19;
then reconsider N = N as internal DirectSumComponents of G,I by ;
take f ; :: thesis: ex N being internal DirectSumComponents of G,I st
( f is bijective & ( for i being Element of I ex qi being Homomorphism of (M . i),(N . i) st
( qi = f * (1ProdHom (M,i)) & qi is bijective ) ) )

take N ; :: thesis: ( f is bijective & ( for i being Element of I ex qi being Homomorphism of (M . i),(N . i) st
( qi = f * (1ProdHom (M,i)) & qi is bijective ) ) )

for i being Element of I ex qi being Homomorphism of (M . i),(N . i) st
( qi = f * (1ProdHom (M,i)) & qi is bijective )
proof
let i be Element of I; :: thesis: ex qi being Homomorphism of (M . i),(N . i) st
( qi = f * (1ProdHom (M,i)) & qi is bijective )

consider qi being Homomorphism of (M . i),(N . i) such that
A31: qi = q . i and
A32: qi is bijective by A8;
take qi ; :: thesis: ( qi = f * (1ProdHom (M,i)) & qi is bijective )
thus ( qi = f * (1ProdHom (M,i)) & qi is bijective ) by A7, A31, A32; :: thesis: verum
end;
hence ( f is bijective & ( for i being Element of I ex qi being Homomorphism of (M . i),(N . i) st
( qi = f * (1ProdHom (M,i)) & qi is bijective ) ) ) by A1; :: thesis: verum