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 H_{1}( 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 = H_{1}(i)
from CLASSES1:sch 2();

A4: for i being object st i in I holds

N . i is strict Subgroup of G

N . i is Group ;

then reconsider N = N as Group-Family of I by A2, GROUP_19:2;

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 H_{2}( 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 = H_{2}(i)
from CLASSES1:sch 2();

reconsider q = q as non empty Function by A6;

( qi = q . i & qi is bijective ) ;

reconsider r = SumMap (M,N,q) as Homomorphism of (sum M),(sum N) ;

A15: r is bijective by A6, A14, GROUP_19:41;

reconsider s = r " as Homomorphism of (sum N),(sum M) by A6, A14, GROUP_19:41, GROUP_6:62;

A16: s is bijective by A15, GROUP_6:63;

reconsider g = f * s as Function ;

reconsider g = g as Homomorphism of (sum N),G ;

A17: g is bijective by A1, A16, GROUP_6:64;

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

g . a = Product a by Th19;

then reconsider N = N as internal DirectSumComponents of G,I by A5, A17, GROUP_19:def 9;

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 )

( qi = f * (1ProdHom (M,i)) & qi is bijective ) ) ) by A1; :: thesis: verum

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 H

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 = H

A4: for i being object st i in I holds

N . i is strict Subgroup of G

proof

then
for i being object st i in I holds
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;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

N . i is Group ;

then reconsider N = N as Group-Family of I by A2, GROUP_19:2;

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 H

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 = H

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 )

then A14:
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 A9, RELAT_1:165;

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 A1, FUNCT_1:52;

A13: fi is onto by A11, FUNCT_2:def 3;

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 A7, A10; :: thesis: qi is bijective

thus qi is bijective by A12, A13, GROUP_6:64; :: thesis: verum

end;( 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 A9, RELAT_1:165;

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 A1, FUNCT_1:52;

A13: fi is onto by A11, FUNCT_2:def 3;

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 A7, A10; :: thesis: qi is bijective

thus qi is bijective by A12, A13, GROUP_6:64; :: thesis: verum

( qi = q . i & qi is bijective ) ;

reconsider r = SumMap (M,N,q) as Homomorphism of (sum M),(sum N) ;

A15: r is bijective by A6, A14, GROUP_19:41;

reconsider s = r " as Homomorphism of (sum N),(sum M) by A6, A14, GROUP_19:41, GROUP_6:62;

A16: s is bijective by A15, GROUP_6:63;

reconsider g = f * s as Function ;

reconsider g = g as Homomorphism of (sum N),G ;

A17: g is bijective by A1, A16, GROUP_6:64;

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

then
for a being finite-support Function of I,G st a in sum N holds
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 A19, FUNCT_2:def 3;

then consider m being object such that

A21: m in [#] (M . i) and

A22: qi . m = n by A20, FUNCT_1:def 3;

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)

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 A7, A18;

A30: m in dom (1ProdHom (M,i)) by A21, FUNCT_2:def 1;

g . ((1ProdHom (N,i)) . n) = f . (s . ((1ProdHom (N,i)) . n)) by A27, A28, FUNCT_1:13

.= f . ((1ProdHom (M,i)) . m) by A15, A24, A25, A26, FUNCT_1:34

.= n by A22, A29, A30, FUNCT_1:13 ;

hence g . ((1ProdHom (N,i)) . n) = n ; :: thesis: verum

end;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 A19, FUNCT_2:def 3;

then consider m being object such that

A21: m in [#] (M . i) and

A22: qi . m = n by A20, FUNCT_1:def 3;

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

then A24:
r . ((1ProdHom (M,i)) . m) = (1ProdHom (N,i)) . n
by A6, A18, A22, GROUP_19:42;
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;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

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 A7, A18;

A30: m in dom (1ProdHom (M,i)) by A21, FUNCT_2:def 1;

g . ((1ProdHom (N,i)) . n) = f . (s . ((1ProdHom (N,i)) . n)) by A27, A28, FUNCT_1:13

.= f . ((1ProdHom (M,i)) . m) by A15, A24, A25, A26, FUNCT_1:34

.= n by A22, A29, A30, FUNCT_1:13 ;

hence g . ((1ProdHom (N,i)) . n) = n ; :: thesis: verum

g . a = Product a by Th19;

then reconsider N = N as internal DirectSumComponents of G,I by A5, A17, GROUP_19:def 9;

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

hence
( f is bijective & ( for i being Element of I ex qi being Homomorphism of (M . i),(N . i) st
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;( 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

( qi = f * (1ProdHom (M,i)) & qi is bijective ) ) ) by A1; :: thesis: verum