let I be non empty set ; :: thesis: for J being non-empty disjoint_valued ManySortedSet of I
for G being Group
for M being DirectSumComponents of G,I
for N being Group-Family of I,J st ( for i being Element of I holds N . i is DirectSumComponents of M . i,J . i ) holds
Union N is DirectSumComponents of G, Union J
let J be non-empty disjoint_valued ManySortedSet of I; :: thesis: for G being Group
for M being DirectSumComponents of G,I
for N being Group-Family of I,J st ( for i being Element of I holds N . i is DirectSumComponents of M . i,J . i ) holds
Union N is DirectSumComponents of G, Union J
let G be Group; :: thesis: for M being DirectSumComponents of G,I
for N being Group-Family of I,J st ( for i being Element of I holds N . i is DirectSumComponents of M . i,J . i ) holds
Union N is DirectSumComponents of G, Union J
let M be DirectSumComponents of G,I; :: thesis: for N being Group-Family of I,J st ( for i being Element of I holds N . i is DirectSumComponents of M . i,J . i ) holds
Union N is DirectSumComponents of G, Union J
let N be Group-Family of I,J; :: thesis: ( ( for i being Element of I holds N . i is DirectSumComponents of M . i,J . i ) implies Union N is DirectSumComponents of G, Union J )
assume A1: for i being Element of I holds N . i is DirectSumComponents of M . i,J . i ; :: thesis: Union N is DirectSumComponents of G, Union J
consider fM2G being Homomorphism of (sum M),G such that
A2: fM2G is bijective by GROUP_19:def 8;
deffunc H₁( object ) -> Element of bool the carrier of (sum (N . (In ($1,I)))) = [#] (sum (N . (In ($1,I))));
consider DS being Function such that
A3: ( dom DS = I & ( for i being object st i in I holds
DS . i = H₁(i) ) ) from FUNCT_1:sch 3();
reconsider DS = DS as ManySortedSet of I by A3, PARTFUN1:def 2, RELAT_1:def 18;
deffunc H₂( object ) -> Element of bool the carrier of (M . (In ($1,I))) = [#] (M . (In ($1,I)));
consider RS being Function such that
A4: ( dom RS = I & ( for i being object st i in I holds
RS . i = H₂(i) ) ) from FUNCT_1:sch 3();
reconsider RS = RS as ManySortedSet of I by A4, PARTFUN1:def 2, RELAT_1:def 18;
defpred S₁[ object , object ] means ex fi being Homomorphism of (sum (N . (In ($1,I)))),(M . (In ($1,I))) st
( fi = $2 & fi is bijective );
A5: for i being Element of I ex y being Element of PFuncs ((Union DS),(Union RS)) st S₁[i,y]

proof

let i be Element of I; :: thesis: ex y being Element of PFuncs ((Union DS),(Union RS)) st S₁[i,y]
N . i is DirectSumComponents of M . i,J . i by A1;
then consider h being Homomorphism of (sum (N . i)),(M . i) such that
A6: h is bijective by GROUP_19:def 8;
A7: In (i,I) = i ;
( DS . i = [#] (sum (N . i)) & RS . i = [#] (M . i) ) by A3, A4, A7;
then ( [#] (sum (N . i)) c= Union DS & [#] (M . i) c= Union RS ) by A3, A4, FUNCT_1:3, ZFMISC_1:74;
then ( dom h c= Union DS & rng h c= Union RS ) ;
then reconsider y = h as Element of PFuncs ((Union DS),(Union RS)) by PARTFUN1:def 3;
take y ; :: thesis: S₁[i,y]
thus S₁[i,y] by A6; :: thesis: verum

end;

consider fBN2M being Function of I,(PFuncs ((Union DS),(Union RS))) such that
A9: for i being Element of I holds S₁[i,fBN2M . i] from FUNCT_2:sch 3(A5);
reconsider fBN2M = fBN2M as ManySortedSet of I ;
set fDN2M = ProductHom (G,M,N,fBN2M);
for i being Element of I ex hi being Homomorphism of ((sum_bundle N) . i),(M . i) st
( hi = fBN2M . i & hi is bijective )

proof

let i be Element of I; :: thesis: ex hi being Homomorphism of ((sum_bundle N) . i),(M . i) st
( hi = fBN2M . i & hi is bijective )
consider fi being Homomorphism of (sum (N . (In (i,I)))),(M . (In (i,I))) such that
A11: ( fi = fBN2M . i & fi is bijective ) by A9;
sum (N . i) = (sum_bundle N) . i by Def7;
then reconsider fi = fi as Homomorphism of ((sum_bundle N) . i),(M . i) ;
take fi ; :: thesis: ( fi = fBN2M . i & fi is bijective )
thus ( fi = fBN2M . i & fi is bijective ) by A11; :: thesis: verum

end;

then A12: ProductHom (G,M,N,fBN2M) is bijective by Def16;
reconsider h = (fM2G * (ProductHom (G,M,N,fBN2M))) * (sum2dsum N) as Homomorphism of (sum (Union N)),G ;
take h ; :: according to GROUP_19:def 8 :: thesis: h is bijective
( fM2G * (ProductHom (G,M,N,fBN2M)) is one-to-one & fM2G * (ProductHom (G,M,N,fBN2M)) is onto ) by A2, A12, FUNCT_2:27;
then ( h is one-to-one & h is onto ) by FUNCT_2:27;
hence h is bijective ; :: thesis: verum