Lm0193:
for I being set
for F being multMagma-Family of I
for x being Element of (product F) holds dom x = I
by GROUP_19:3;
Lm0194:
for I being non empty set
for F being multMagma-Family of I
for x being Element of I holds (Carrier F) . x = [#] (F . x)
by GROUP_19:4;
Lm0195:
for I being non empty set
for F being multMagma-Family of I
for x being Function
for i being Element of I st x in product F holds
x . i in F . i
by GROUP_19:5;
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
ThXX:
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 is bijective
by GROUP_6:63;
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
Th37:
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 is bijective
by GROUP_6:63;
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 )
;
existence
ex b1 being Homomorphism of (dsum N),(sum M) st
( b1 = SumMap ((sum_bundle N),M,h) & b1 is bijective )
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;