environ
vocabularies HIDDEN, FINSEQ_1, FUNCT_1, RELAT_1, RLVECT_2, CARD_3, TARSKI, BINOP_1, GROUP_1, GROUP_2, CARD_1, FUNCT_4, GROUP_6, GROUP_7, FUNCT_7, FUNCOP_1, ALGSTR_0, GROUP_12, PARTFUN1, FUNCT_2, SUBSET_1, XBOOLE_0, STRUCT_0, NAT_1, FINSET_1, ZFMISC_1, PBOOLE, REALSET1, GROUP_4, PRE_POLY, UPROOTS, GROUP_19, GROUP_20, MSSUBFAM, SEMI_AF1, VECTMETR, PROB_2, MONOID_0, GROUP_21;
notations HIDDEN, TARSKI, XBOOLE_0, SUBSET_1, ZFMISC_1, RELAT_1, FUNCT_1, ORDINAL1, RELSET_1, PARTFUN1, FUNCT_2, BINOP_1, DOMAIN_1, FUNCOP_1, REALSET1, FUNCT_4, FINSET_1, CARD_1, PBOOLE, CARD_3, FINSEQ_1, FUNCT_7, PROB_2, STRUCT_0, ALGSTR_0, GROUP_1, GROUP_2, GROUP_4, GROUP_6, MONOID_0, PRALG_1, GRSOLV_1, GROUP_7, GROUP_12, GROUP_17, GROUP_19, GROUP_20;
definitions FUNCT_2, GROUP_19;
theorems FUNCT_1, CARD_3, FUNCT_2, FUNCOP_1, TARSKI, GROUP_1, GROUP_2, FUNCT_4, FINSEQ_1, GROUP_4, GROUP_6, XTUPLE_0, XBOOLE_0, RELAT_1, GROUP_7, SUBSET_1, FUNCT_7, BINOP_1, CARD_2, XBOOLE_1, ALGSTR_0, GROUP_12, PARTFUN1, ZFMISC_1, CARD_1, GROUP_17, FINSET_1, GROUP_19, GROUP_20, PROB_2;
schemes FUNCT_1, FUNCT_2, CLASSES1;
registrations XBOOLE_0, STRUCT_0, GROUP_2, MONOID_0, ORDINAL1, NAT_1, FUNCT_2, CARD_1, GROUP_7, MSAFREE, PARTFUN1, RELSET_1, REALSET1, FINSEQ_1, SUBSET_1, FINSET_1, RELAT_1, FUNCT_1, PBOOLE, GROUP_6, GROUP_19;
constructors HIDDEN, REALSET1, FUNCT_4, MONOID_0, PRALG_1, GROUP_4, FUNCT_7, RELSET_1, WELLORD2, FUNCT_3, GROUP_17, GRSOLV_1, PROB_2, GROUP_19, GROUP_20;
requirements HIDDEN, NUMERALS, BOOLE, SUBSET;
equalities STRUCT_0, GRSOLV_1, GROUP_19, REALSET1;
expansions STRUCT_0, TARSKI, GROUP_19, PROB_2, FUNCT_1, RELAT_1;
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;