:: Conservation Rules of Direct Sum Decomposition of Groups
:: by Kazuhisa Nakasho , Hiroshi Yamazaki , Hiroyuki Okazaki and Yasunari Shidama
::
:: Received December 31, 2015
:: Copyright (c) 2015-2021 Association of Mizar Users


definition
let I, J be non empty set ;
let a be Function of I,J;
let F be multMagma-Family of J;
:: original: *
redefine func F * a -> multMagma-Family of I;
correctness
coherence
a * F is multMagma-Family of I;
proof end;
end;

definition
let I, J be non empty set ;
let a be Function of I,J;
let F be Group-Family of J;
:: original: *
redefine func F * a -> Group-Family of I;
correctness
coherence
a * F is Group-Family of I;
proof end;
end;

definition
let I, J be non empty set ;
let a be Function of I,J;
let G be Group;
let F be Subgroup-Family of J,G;
func F * a -> Subgroup-Family of I,G equals :: GROUP_21:def 1
F * a;
correctness
coherence
F * a is Subgroup-Family of I,G;
proof end;
end;

:: deftheorem defines * GROUP_21:def 1 :
for I, J being non empty set
for a being Function of I,J
for G being Group
for F being Subgroup-Family of J,G holds F * a = F * a;

scheme :: GROUP_21:sch 1
Sch1{ F1() -> set , F2() -> 1-sorted , F3( Element of F2()) -> set } :
ex f being Function st
( dom f = F1() & ( for x being Element of F2() st x in F1() holds
f . x = F3(x) ) )
proof end;

registration
let I be set ;
cluster Relation-like non-empty I -defined Function-like total disjoint_valued for set ;
correctness
existence
ex b1 being ManySortedSet of I st
( b1 is non-empty & b1 is disjoint_valued );
proof end;
end;

theorem Th30: :: GROUP_21:1
for f being non-empty disjoint_valued Function st Union f is finite holds
dom f is finite
proof end;

theorem Th35: :: GROUP_21:2
for X, Y being non empty set
for X0, Y0 being set
for f being Function of X,Y st f is bijective & rng (f | X0) = Y0 holds
(f | X0) " = (f ") | Y0
proof end;

:: for substitution of subscript set
theorem Th1: :: GROUP_21:3
for I, J being non empty set
for a being Function of I,J
for F being multMagma-Family of J
for x being Element of (product F) holds x * a in product (F * a)
proof end;

definition
let I, J be non empty set ;
let a be Function of I,J;
let F be multMagma-Family of J;
func trans_prod (F,a) -> Function of (product F),(product (F * a)) means :Def2: :: GROUP_21:def 2
 for x being Element of (product F) holds it . x = x * a;
existence
ex b1 being Function of (product F),(product (F * a)) st
for x being Element of (product F) holds b1 . x = x * a
proof end;
uniqueness
for b1, b2 being Function of (product F),(product (F * a)) st ( for x being Element of (product F) holds b1 . x = x * a ) & ( for x being Element of (product F) holds b2 . x = x * a ) holds
b1 = b2
proof end;
end;

:: deftheorem Def2 defines trans_prod GROUP_21:def 2 :
for I, J being non empty set
for a being Function of I,J
for F being multMagma-Family of J
for b5 being Function of (product F),(product (F * a)) holds
( b5 = trans_prod (F,a) iff for x being Element of (product F) holds b5 . x = x * a );

theorem Th2: :: GROUP_21:4
for I, J being non empty set
for a being Function of I,J
for F being multMagma-Family of J holds trans_prod (F,a) is multiplicative
proof end;

definition
let I, J be non empty set ;
let a be Function of I,J;
let F be Group-Family of J;
:: original: trans_prod
redefine func trans_prod (F,a) -> Homomorphism of (product F),(product (F * a));
correctness
coherence
trans_prod (F,a) is Homomorphism of (product F),(product (F * a));
by Th2;
end;

theorem Th3: :: GROUP_21:5
for I, J being non empty set
for a being Function of I,J
for F being multMagma-Family of J
for y being Element of (product (F * a)) st a is bijective holds
y * (a ") in product F
proof end;

theorem Th4: :: GROUP_21:6
for I, J being non empty set
for a being Function of I,J
for x, y being Function st dom x = I & dom y = J & a is bijective holds
( x = y * a iff y = x * (a ") )
proof end;

theorem Th5: :: GROUP_21:7
for I, J being non empty set
for F being multMagma-Family of J
for a being Function of I,J st a is bijective holds
( dom (trans_prod (F,a)) = [#] (product F) & rng (trans_prod (F,a)) = [#] (product (F * a)) )
proof end;

theorem Th6: :: GROUP_21:8
for I, J being non empty set
for a being Function of I,J
for F being multMagma-Family of J st a is bijective holds
trans_prod (F,a) is bijective
proof end;

theorem Th7: :: GROUP_21:9
for I, J being non empty set
for a being Function of I,J
for F being Group-Family of J
for x being Function holds a .: (support ((x * a),(F * a))) c= support (x,F)
proof end;

theorem Th8: :: GROUP_21:10
for I, J being non empty set
for a being Function of I,J
for F being Group-Family of J
for x being Function st a is onto holds
support (x,F) c= a .: (support ((x * a),(F * a)))
proof end;

theorem Th9: :: GROUP_21:11
for I, J being non empty set
for a being Function of I,J
for F being Group-Family of J
for x being Function st a is one-to-one & x in sum F holds
x * a in sum (F * a)
proof end;

theorem Th10: :: GROUP_21:12
for I, J being non empty set
for a being Function of I,J
for F being Group-Family of J
for x being Function st a is bijective holds
( x in sum F iff ( x * a in sum (F * a) & dom x = J ) )
proof end;

definition
let I, J be non empty set ;
let a be Function of I,J;
let F be Group-Family of J;
assume A1: a is bijective ;
func trans_sum (F,a) -> Function of (sum F),(sum (F * a)) equals :Def3: :: GROUP_21:def 3
(trans_prod (F,a)) | (sum F);
correctness
coherence
(trans_prod (F,a)) | (sum F) is Function of (sum F),(sum (F * a));
proof end;
end;

:: deftheorem Def3 defines trans_sum GROUP_21:def 3 :
for I, J being non empty set
for a being Function of I,J
for F being Group-Family of J st a is bijective holds
trans_sum (F,a) = (trans_prod (F,a)) | (sum F);

theorem Th11: :: GROUP_21:13
for G, H being Group
for H0 being Subgroup of H
for f being Homomorphism of G,H st rng f c= [#] H0 holds
f is Homomorphism of G,H0
proof end;

theorem TT: :: GROUP_21:14
for I, J being non empty set
for a being Function of I,J
for F being Group-Family of J st a is bijective holds
trans_sum (F,a) is Homomorphism of (sum F),(sum (F * a))
proof end;

theorem Th12: :: GROUP_21:15
for I, J being non empty set
for a being Function of I,J
for F being Group-Family of J st a is bijective holds
trans_sum (F,a) is bijective
proof end;

:: independent from subscript set
theorem Th13: :: GROUP_21:16
for G being Group
for I, J being non empty set
for F being DirectSumComponents of G,J
for a being Function of I,J st a is bijective holds
F * a is DirectSumComponents of G,I
proof end;

theorem :: GROUP_21:17
for I being non empty set
for G being Group
for F being internal DirectSumComponents of G,I holds F is Subgroup-Family of I,G
proof end;

theorem Th15: :: GROUP_21:18
for I, J being non empty set
for G being Group
for x being Function of I,G
for y being Function of J,G
for a being Function of I,J st a is onto & x = y * a holds
support y = a .: (support x)
proof end;

theorem Th16: :: GROUP_21:19
for I, J being non empty set
for G being commutative Group
for x being finite-support Function of I,G
for y being finite-support Function of J,G
for a being Function of I,J st a is bijective & x = y * a holds
Product x = Product y
proof end;

theorem :: GROUP_21:20
for I, J being non empty set
for G being Group
for x being finite-support Function of I,G
for y being finite-support Function of J,G
for a being Function of I,J st a is bijective & x = y * a & ( for i, j being Element of I holds (x . i) * (x . j) = (x . j) * (x . i) ) holds
Product x = Product y
proof end;

theorem :: GROUP_21:21
for G being Group
for I, J being non empty set
for F being internal DirectSumComponents of G,J
for a being Function of I,J st a is bijective holds
F * a is internal DirectSumComponents of G,I
proof end;

definition
let I be non empty set ;
let J be ManySortedSet of I;
mode multMagma-Family of I,J -> ManySortedSet of I means :Def4: :: GROUP_21:def 4
 for i being Element of I holds it . i is multMagma-Family of J . i;
existence
ex b1 being ManySortedSet of I st
for i being Element of I holds b1 . i is multMagma-Family of J . i
proof end;
end;

:: deftheorem Def4 defines multMagma-Family GROUP_21:def 4 :
for I being non empty set
for J, b3 being ManySortedSet of I holds
( b3 is multMagma-Family of I,J iff for i being Element of I holds b3 . i is multMagma-Family of J . i );

definition
let I be non empty set ;
let J be ManySortedSet of I;
mode Group-Family of I,J -> multMagma-Family of I,J means :Def5: :: GROUP_21:def 5
 for i being Element of I holds it . i is Group-Family of J . i;
existence
ex b1 being multMagma-Family of I,J st
for i being Element of I holds b1 . i is Group-Family of J . i
proof end;
end;

:: deftheorem Def5 defines Group-Family GROUP_21:def 5 :
for I being non empty set
for J being ManySortedSet of I
for b3 being multMagma-Family of I,J holds
( b3 is Group-Family of I,J iff for i being Element of I holds b3 . i is Group-Family of J . i );

definition
let I be non empty set ;
let J be ManySortedSet of I;
let N be multMagma-Family of I,J;
let i be Element of I;
:: original: .
redefine func N . i -> multMagma-Family of J . i;
correctness
coherence
N . i is multMagma-Family of J . i;
by Def4;
end;

definition
let I be non empty set ;
let J be ManySortedSet of I;
let N be Group-Family of I,J;
let i be Element of I;
:: original: .
redefine func N . i -> Group-Family of J . i;
correctness
coherence
N . i is Group-Family of J . i;
by Def5;
end;

definition
let I be non empty set ;
let J be disjoint_valued ManySortedSet of I;
let F be Group-Family of I,J;
:: original: Union
redefine func Union F -> Group-Family of Union J;
correctness
coherence
Union F is Group-Family of Union J;
proof end;
end;

theorem Th19: :: GROUP_21:22
for I being non empty set
for J being disjoint_valued ManySortedSet of I
for F being Group-Family of I,J
for j being Element of I
for i being object st i in J . j holds
(Union F) . i = (F . j) . i
proof end;

definition
let I be non empty set ;
let J be ManySortedSet of I;
let F be multMagma-Family of I,J;
func prod_bundle F -> multMagma-Family of I means :Def6: :: GROUP_21:def 6
 for i being Element of I holds it . i = product (F . i);
existence
ex b1 being multMagma-Family of I st
for i being Element of I holds b1 . i = product (F . i)
proof end;
uniqueness
for b1, b2 being multMagma-Family of I st ( for i being Element of I holds b1 . i = product (F . i) ) & ( for i being Element of I holds b2 . i = product (F . i) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def6 defines prod_bundle GROUP_21:def 6 :
for I being non empty set
for J being ManySortedSet of I
for F being multMagma-Family of I,J
for b4 being multMagma-Family of I holds
( b4 = prod_bundle F iff for i being Element of I holds b4 . i = product (F . i) );

definition
let I be non empty set ;
let J be ManySortedSet of I;
let F be Group-Family of I,J;
:: original: prod_bundle
redefine func prod_bundle F -> Group-Family of I;
correctness
coherence
prod_bundle F is Group-Family of I;
proof end;
end;

definition
let I be non empty set ;
let J be ManySortedSet of I;
let F be Group-Family of I,J;
func sum_bundle F -> Group-Family of I means :Def7: :: GROUP_21:def 7
 for i being Element of I holds it . i = sum (F . i);
existence
ex b1 being Group-Family of I st
for i being Element of I holds b1 . i = sum (F . i)
proof end;
uniqueness
for b1, b2 being Group-Family of I st ( for i being Element of I holds b1 . i = sum (F . i) ) & ( for i being Element of I holds b2 . i = sum (F . i) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def7 defines sum_bundle GROUP_21:def 7 :
for I being non empty set
for J being ManySortedSet of I
for F being Group-Family of I,J
for b4 being Group-Family of I holds
( b4 = sum_bundle F iff for i being Element of I holds b4 . i = sum (F . i) );

definition
let I be non empty set ;
let J be ManySortedSet of I;
let F be multMagma-Family of I,J;
func dprod F -> multMagma equals :: GROUP_21:def 8
 product (prod_bundle F);
correctness
coherence
product (prod_bundle F) is multMagma ;
;
end;

:: deftheorem defines dprod GROUP_21:def 8 :
for I being non empty set
for J being ManySortedSet of I
for F being multMagma-Family of I,J holds dprod F = product (prod_bundle F);

registration
let I be non empty set ;
let J be non-empty ManySortedSet of I;
let F be multMagma-Family of I,J;
cluster dprod F -> non empty constituted-Functions ;
correctness
coherence
( not dprod F is empty & dprod F is constituted-Functions );
;
end;

registration
let I be non empty set ;
let J be non-empty ManySortedSet of I;
let F be Group-Family of I,J;
cluster dprod F -> Group-like associative ;
coherence
( dprod F is Group-like & dprod F is associative )
proof end;
end;

definition
let I be non empty set ;
let J be non-empty ManySortedSet of I;
let F be Group-Family of I,J;
func dsum F -> Group equals :: GROUP_21:def 9
 sum (sum_bundle F);
correctness
coherence
sum (sum_bundle F) is Group;
;
end;

:: deftheorem defines dsum GROUP_21:def 9 :
for I being non empty set
for J being non-empty ManySortedSet of I
for F being Group-Family of I,J holds dsum F = sum (sum_bundle F);

registration
let I be non empty set ;
let J be non-empty ManySortedSet of I;
let F be Group-Family of I,J;
cluster dsum F -> constituted-Functions ;
correctness
coherence
( not dsum F is empty & dsum F is constituted-Functions );
;
end;

theorem Th20: :: GROUP_21:23
for I being non empty set
for F1, F2 being Group-Family of I st ( for i being Element of I holds F1 . i is Subgroup of F2 . i ) holds
product F1 is Subgroup of product F2
proof end;

theorem :: GROUP_21:24
for I being non empty set
for F1, F2 being Group-Family of I st ( for i being Element of I holds F1 . i is Subgroup of F2 . i ) holds
sum F1 is Subgroup of sum F2
proof end;

theorem Th22: :: GROUP_21:25
for I being non empty set
for J being non-empty ManySortedSet of I
for F being Group-Family of I,J holds dsum F is Subgroup of dprod F
proof end;

definition
let I be non empty set ;
let J be non-empty disjoint_valued ManySortedSet of I;
let F be Group-Family of I,J;
:: original: dsum
redefine func dsum F -> Subgroup of dprod F;
correctness
coherence
dsum F is Subgroup of dprod F;
by Th22;
end;

definition
let I be non empty set ;
let J be non-empty disjoint_valued ManySortedSet of I;
let F be Group-Family of I,J;
func dprod2prod F -> Homomorphism of (dprod F),(product (Union F)) means :Def10: :: GROUP_21:def 10
 for x being Element of (dprod F)
for i being Element of I holds x . i = (it . x) | (J . i);
existence
ex b1 being Homomorphism of (dprod F),(product (Union F)) st
for x being Element of (dprod F)
for i being Element of I holds x . i = (b1 . x) | (J . i)
proof end;
uniqueness
for b1, b2 being Homomorphism of (dprod F),(product (Union F)) st ( for x being Element of (dprod F)
for i being Element of I holds x . i = (b1 . x) | (J . i) ) & ( for x being Element of (dprod F)
for i being Element of I holds x . i = (b2 . x) | (J . i) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def10 defines dprod2prod GROUP_21:def 10 :
for I being non empty set
for J being non-empty disjoint_valued ManySortedSet of I
for F being Group-Family of I,J
for b4 being Homomorphism of (dprod F),(product (Union F)) holds
( b4 = dprod2prod F iff for x being Element of (dprod F)
for i being Element of I holds x . i = (b4 . x) | (J . i) );

theorem Th23: :: GROUP_21:26
for I being non empty set
for J being non-empty disjoint_valued ManySortedSet of I
for F being Group-Family of I,J
for y being Element of (product (Union F))
for i being Element of I holds y | (J . i) in product (F . i)
proof end;

Th24: for I being non empty set
for J being non-empty disjoint_valued ManySortedSet of I
for F being Group-Family of I,J holds dprod2prod F is bijective
proof end;

registration
let I be non empty set ;
let J be non-empty disjoint_valued ManySortedSet of I;
let F be Group-Family of I,J;
cluster dprod2prod F -> bijective ;
coherence
dprod2prod F is bijective by Th24;
end;

definition
let I be non empty set ;
let J be non-empty disjoint_valued ManySortedSet of I;
let F be Group-Family of I,J;
func prod2dprod F -> Homomorphism of (product (Union F)),(dprod F) equals :: GROUP_21:def 11
(dprod2prod F) " ;
correctness
coherence
(dprod2prod F) " is Homomorphism of (product (Union F)),(dprod F);
by GROUP_6:62;
end;

:: deftheorem defines prod2dprod GROUP_21:def 11 :
for I being non empty set
for J being non-empty disjoint_valued ManySortedSet of I
for F being Group-Family of I,J holds prod2dprod F = (dprod2prod F) " ;

theorem Th25: :: GROUP_21:27
for I being non empty set
for J being non-empty disjoint_valued ManySortedSet of I
for F being Group-Family of I,J
for x being Element of (product (Union F))
for i being Element of I holds x | (J . i) = ((prod2dprod F) . x) . i
proof end;

registration
let I be non empty set ;
let J be non-empty disjoint_valued ManySortedSet of I;
let F be Group-Family of I,J;
cluster prod2dprod F -> bijective ;
coherence
prod2dprod F is bijective by GROUP_6:63;
end;

theorem :: GROUP_21:28
for I being non empty set
for J being non-empty disjoint_valued ManySortedSet of I
for F being Group-Family of I,J holds prod2dprod F = (dprod2prod F) " ;

definition
let I be non empty set ;
let J be non-empty disjoint_valued ManySortedSet of I;
let F be Group-Family of I,J;
let x be Function;
func supp_restr (x,F) -> disjoint_valued ManySortedSet of I means :Def12: :: GROUP_21:def 12
 for i being Element of I holds it . i = support ((x | (J . i)),(F . i));
existence
ex b1 being disjoint_valued ManySortedSet of I st
for i being Element of I holds b1 . i = support ((x | (J . i)),(F . i))
proof end;
uniqueness
for b1, b2 being disjoint_valued ManySortedSet of I st ( for i being Element of I holds b1 . i = support ((x | (J . i)),(F . i)) ) & ( for i being Element of I holds b2 . i = support ((x | (J . i)),(F . i)) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def12 defines supp_restr GROUP_21:def 12 :
for I being non empty set
for J being non-empty disjoint_valued ManySortedSet of I
for F being Group-Family of I,J
for x being Function
for b5 being disjoint_valued ManySortedSet of I holds
( b5 = supp_restr (x,F) iff for i being Element of I holds b5 . i = support ((x | (J . i)),(F . i)) );

theorem Th28: :: GROUP_21:29
for I being non empty set
for J being non-empty disjoint_valued ManySortedSet of I
for F being Group-Family of I,J
for x being Function holds support (x,(Union F)) = Union (supp_restr (x,F))
proof end;

theorem Th29: :: GROUP_21:30
for I being non empty set
for J being non-empty disjoint_valued ManySortedSet of I
for F being Group-Family of I,J
for x, y, z being Function st z in dprod F & x = (dprod2prod F) . z holds
( (supp_restr (x,F)) | (support (z,(sum_bundle F))) is non-empty disjoint_valued ManySortedSet of support (z,(sum_bundle F)) & support (x,(Union F)) = Union ((supp_restr (x,F)) | (support (z,(sum_bundle F)))) )
proof end;

theorem Th31: :: GROUP_21:31
for I being non empty set
for J being non-empty disjoint_valued ManySortedSet of I
for F being Group-Family of I,J
for y being Function st y in sum (Union F) holds
ex x being Function st
( y = (dprod2prod F) . x & x in dsum F )
proof end;

theorem Th32: :: GROUP_21:32
for I being non empty set
for J being non-empty disjoint_valued ManySortedSet of I
for F being Group-Family of I,J
for x, y being Function st x in dsum F & x in dsum F holds
(dprod2prod F) . x in sum (Union F)
proof end;

theorem Th33: :: GROUP_21:33
for I being non empty set
for J being non-empty disjoint_valued ManySortedSet of I
for F being Group-Family of I,J holds rng ((dprod2prod F) | (dsum F)) = [#] (sum (Union F))
proof end;

definition
let I be non empty set ;
let J be non-empty disjoint_valued ManySortedSet of I;
let F be Group-Family of I,J;
func dsum2sum F -> Homomorphism of (dsum F),(sum (Union F)) equals :: GROUP_21:def 13
(dprod2prod F) | (dsum F);
correctness
coherence
(dprod2prod F) | (dsum F) is Homomorphism of (dsum F),(sum (Union F));
proof end;
end;

:: deftheorem defines dsum2sum GROUP_21:def 13 :
for I being non empty set
for J being non-empty disjoint_valued ManySortedSet of I
for F being Group-Family of I,J holds dsum2sum F = (dprod2prod F) | (dsum F);

Th34: for I being non empty set
for J being non-empty disjoint_valued ManySortedSet of I
for F being Group-Family of I,J holds dsum2sum F is bijective
proof end;

registration
let I be non empty set ;
let J be non-empty disjoint_valued ManySortedSet of I;
let F be Group-Family of I,J;
cluster dsum2sum F -> bijective ;
coherence
dsum2sum F is bijective by Th34;
end;

definition
let I be non empty set ;
let J be non-empty disjoint_valued ManySortedSet of I;
let F be Group-Family of I,J;
func sum2dsum F -> Homomorphism of (sum (Union F)),(dsum F) equals :: GROUP_21:def 14
(dsum2sum F) " ;
correctness
coherence
(dsum2sum F) " is Homomorphism of (sum (Union F)),(dsum F);
by GROUP_6:62;
end;

:: deftheorem defines sum2dsum GROUP_21:def 14 :
for I being non empty set
for J being non-empty disjoint_valued ManySortedSet of I
for F being Group-Family of I,J holds sum2dsum F = (dsum2sum F) " ;

theorem Th36: :: GROUP_21:34
for I being non empty set
for J being non-empty disjoint_valued ManySortedSet of I
for F being Group-Family of I,J holds sum2dsum F = (prod2dprod F) | (sum (Union F))
proof end;

registration
let I be non empty set ;
let J be non-empty disjoint_valued ManySortedSet of I;
let F be Group-Family of I,J;
cluster sum2dsum F -> bijective ;
coherence
sum2dsum F is bijective by GROUP_6:63;
end;

theorem :: GROUP_21:35
for I being non empty set
for J being non-empty disjoint_valued ManySortedSet of I
for F being Group-Family of I,J holds dsum2sum F = (sum2dsum F) " by FUNCT_1:43;

definition
let I be non empty set ;
let G be Group;
let F be internal DirectSumComponents of G,I;
func InterHom F -> Homomorphism of (sum F),G means :Def15: :: GROUP_21:def 15
( it is bijective & ( for x being finite-support Function of I,G st x in sum F holds
it . x = Product x ) );
existence
ex b1 being Homomorphism of (sum F),G st
( b1 is bijective & ( for x being finite-support Function of I,G st x in sum F holds
b1 . x = Product x ) ) by GROUP_19:def 9;
uniqueness
for b1, b2 being Homomorphism of (sum F),G st b1 is bijective & ( for x being finite-support Function of I,G st x in sum F holds
b1 . x = Product x ) & b2 is bijective & ( for x being finite-support Function of I,G st x in sum F holds
b2 . x = Product x ) holds
b1 = b2
proof end;
end;

:: deftheorem Def15 defines InterHom GROUP_21:def 15 :
for I being non empty set
for G being Group
for F being internal DirectSumComponents of G,I
for b4 being Homomorphism of (sum F),G holds
( b4 = InterHom F iff ( b4 is bijective & ( for x being finite-support Function of I,G st x in sum F holds
b4 . x = Product x ) ) );

definition
let I be non empty set ;
let J be non-empty disjoint_valued ManySortedSet of I;
let G be Group;
let M be DirectSumComponents of G,I;
let N be Group-Family of I,J;
let h be ManySortedSet of I;
assume A2: for i being Element of I ex hi being Homomorphism of ((sum_bundle N) . i),(M . i) st
( hi = h . i & hi is bijective ) ;
func ProductHom (G,M,N,h) -> Homomorphism of (dsum N),(sum M) means :Def16: :: GROUP_21:def 16
( it = SumMap ((sum_bundle N),M,h) & it is bijective );
existence
ex b1 being Homomorphism of (dsum N),(sum M) st
( b1 = SumMap ((sum_bundle N),M,h) & b1 is bijective )
proof end;
uniqueness
for b1, b2 being Homomorphism of (dsum N),(sum M) st b1 = SumMap ((sum_bundle N),M,h) & b1 is bijective & b2 = SumMap ((sum_bundle N),M,h) & b2 is bijective holds
b1 = b2 ;
end;

:: deftheorem Def16 defines ProductHom GROUP_21:def 16 :
for I being non empty set
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
for h being ManySortedSet of I st ( for i being Element of I ex hi being Homomorphism of ((sum_bundle N) . i),(M . i) st
( hi = h . i & hi is bijective ) ) holds
for b7 being Homomorphism of (dsum N),(sum M) holds
( b7 = ProductHom (G,M,N,h) iff ( b7 = SumMap ((sum_bundle N),M,h) & b7 is bijective ) );

theorem Th39: :: GROUP_21:36
for I being non empty set
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
proof end;

theorem Th40: :: GROUP_21:37
for I being non empty set
for J being non-empty disjoint_valued ManySortedSet of I
for G being Group
for M being internal DirectSumComponents of G,I
for N being Group-Family of I,J st ( for i being Element of I holds N . i is internal DirectSumComponents of M . i,J . i ) holds
Union N is internal DirectSumComponents of G, Union J
proof end;

theorem Th41: :: GROUP_21:38
for I being non empty set
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
proof end;

theorem :: GROUP_21:39
for I being non empty set
for J being non-empty disjoint_valued ManySortedSet of I
for G being Group
for M being Subgroup-Family of I,G
for N being Group-Family of I,J st Union N is internal DirectSumComponents of G, Union J & ( for i being Element of I holds N . i is internal DirectSumComponents of M . i,J . i ) holds
M is internal DirectSumComponents of G,I
proof end;

::
:: trivial groups addition preservance
::
:: Corollary of Th39
::
theorem Th43: :: GROUP_21:40
for I2 being non empty set
for F2 being Group-Family of I2 st ( for i being Element of I2 holds card (F2 . i) = 1 ) holds
card the carrier of (sum F2) = 1
proof end;

theorem Th44: :: GROUP_21:41
for I being non empty set
for G being Group
for x being finite-support Function of I,G st ( for i being object st i in I holds
x . i = 1_ G ) holds
Product x = 1_ G
proof end;

theorem Th45: :: GROUP_21:42
for I being non empty set
for G being Group
for x being finite-support Function of I,G
for a being Element of G st I = {1,2} & x = <*a,(1_ G)*> holds
Product x = a
proof end;

theorem :: GROUP_21:43
for G being Group
for I1, I2 being non empty set
for F1 being DirectSumComponents of G,I1
for F2 being Group-Family of I2 st I1 misses I2 & ( for i being Element of I2 holds card (F2 . i) = 1 ) holds
F1 +* F2 is DirectSumComponents of G,I1 \/ I2
proof end;

theorem :: GROUP_21:44
for G being Group
for I1, I2 being non empty set
for F1 being internal DirectSumComponents of G,I1
for F2 being Subgroup-Family of I2,G st I1 misses I2 & F2 = I2 --> ((1). G) holds
F1 +* F2 is internal DirectSumComponents of G,I1 \/ I2
proof end;