let I be non empty set ; :: thesis: for J being non-empty disjoint_valued ManySortedSet of I
for G being Group
for M being Group-Family of I
for N being Group-Family of I,J st Union N is DirectSumComponents of G, Union J & ( for i being Element of I holds N . i is DirectSumComponents of M . i,J . i ) holds
M is DirectSumComponents of G,I
let J be non-empty disjoint_valued ManySortedSet of I; :: thesis: for G being Group
for M being Group-Family of I
for N being Group-Family of I,J st Union N is DirectSumComponents of G, Union J & ( for i being Element of I holds N . i is DirectSumComponents of M . i,J . i ) holds
M is DirectSumComponents of G,I
let G be Group; :: thesis: for M being Group-Family of I
for N being Group-Family of I,J st Union N is DirectSumComponents of G, Union J & ( for i being Element of I holds N . i is DirectSumComponents of M . i,J . i ) holds
M is DirectSumComponents of G,I
let M be Group-Family of I; :: thesis: for N being Group-Family of I,J st Union N is DirectSumComponents of G, Union J & ( for i being Element of I holds N . i is DirectSumComponents of M . i,J . i ) holds
M is DirectSumComponents of G,I
let N be Group-Family of I,J; :: thesis: ( Union N is DirectSumComponents of G, Union J & ( for i being Element of I holds N . i is DirectSumComponents of M . i,J . i ) implies M is DirectSumComponents of G,I )
assume that
A1: Union N is DirectSumComponents of G, Union J and
A2: for i being Element of I holds N . i is DirectSumComponents of M . i,J . i ; :: thesis: M is DirectSumComponents of G,I
set UN = Union N;
consider fNtoG being Homomorphism of (sum (Union N)),G such that
A3: fNtoG is bijective by A1, GROUP_19:def 8;
deffunc H₁( object ) -> set = the carrier of (sum (N . (In ($1,I))));
consider DS being Function such that
A4: ( 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 A4, PARTFUN1:def 2, RELAT_1:def 18;
deffunc H₂( object ) -> set = the carrier of (M . (In ($1,I)));
consider RS being Function such that
A5: ( 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 A5, PARTFUN1:def 2, RELAT_1:def 18;
defpred S₁[ object , object ] means ex fi being Homomorphism of (M . (In ($1,I))),(sum (N . (In ($1,I)))) st
( fi = $2 & fi is bijective );
A6: for i being Element of I ex y being Element of PFuncs ((Union RS),(Union DS)) st S₁[i,y]

proof

let i be Element of I; :: thesis: ex y being Element of PFuncs ((Union RS),(Union DS)) st S₁[i,y]
N . i is DirectSumComponents of M . i,J . i by A2;
then consider g being Homomorphism of (sum (N . i)),(M . i) such that
A7: g is bijective by GROUP_19:def 8;
reconsider h = g " as Homomorphism of (M . i),(sum (N . i)) by A7, GROUP_6:62;
A8: h is bijective by A7, GROUP_6:63;
A9: In (i,I) = i ;
( DS . i in rng DS & RS . i in rng RS ) by A4, A5, FUNCT_1:3;
then ( the carrier of (sum (N . i)) in rng DS & the carrier of (M . i) in rng RS ) by A4, A5, A9;
then ( the carrier of (sum (N . i)) c= Union DS & the carrier of (M . i) c= Union RS ) by ZFMISC_1:74;
then ( dom h c= Union RS & rng h c= Union DS ) ;
then reconsider y = h as Element of PFuncs ((Union RS),(Union DS)) by PARTFUN1:def 3;
take y ; :: thesis: S₁[i,y]
thus ex h being Homomorphism of (M . (In (i,I))),(sum (N . (In (i,I)))) st
( h = y & h is bijective ) by A8; :: thesis: verum

end;

consider fMtoBN being Function of I,(PFuncs ((Union RS),(Union DS))) such that
A10: for i being Element of I holds S₁[i,fMtoBN . i] from FUNCT_2:sch 3(A6);
A11: dom fMtoBN = I by FUNCT_2:def 1;
reconsider fMtoBN = fMtoBN as ManySortedSet of I ;
reconsider fMtoDN = SumMap (M,(sum_bundle N),fMtoBN) as Homomorphism of (sum M),(dsum N) ;
for i being Element of I ex hi being Homomorphism of (M . i),((sum_bundle N) . i) st
( hi = fMtoBN . i & hi is bijective )

proof

let i be Element of I; :: thesis: ex hi being Homomorphism of (M . i),((sum_bundle N) . i) st
( hi = fMtoBN . i & hi is bijective )
consider fi being Homomorphism of (M . (In (i,I))),(sum (N . (In (i,I)))) such that
A13: ( fi = fMtoBN . i & fi is bijective ) by A10;
sum (N . (In (i,I))) = (sum_bundle N) . i by Def7;
hence ex hi being Homomorphism of (M . i),((sum_bundle N) . i) st
( hi = fMtoBN . i & hi is bijective ) by A13; :: thesis: verum

end;

then A14: fMtoDN is bijective by A11, GROUP_19:41;
reconsider h = (fNtoG * (dsum2sum N)) * fMtoDN as Homomorphism of (sum M),G ;
take h ; :: according to GROUP_19:def 8 :: thesis: h is bijective
A15: ( fNtoG * (dsum2sum N) is one-to-one & fNtoG * (dsum2sum N) is onto ) by A3, FUNCT_2:27;
( h is one-to-one & h is onto ) by A14, A15, FUNCT_2:27;
hence h is bijective ; :: thesis: verum