let I be non empty set ; for G being Group
for i being object st i in I holds
ex F being Group-Family of I ex h being Homomorphism of (sum F),G st
( h is bijective & F = (I --> ((1). G)) +* ({i} --> G) & ( for j being Element of I holds 1_ (F . j) = 1_ G ) & ( for x being Element of (sum F) holds h . x = x . i ) & ( for x being Element of (sum F) ex J being finite Subset of I ex a being ManySortedSet of J st
( J c= {i} & J = support (x,F) & ( support (x,F) = {} or support (x,F) = {i} ) & x = (1_ (product F)) +* a & ( for j being Element of I st j in I \ J holds
x . j = 1_ (F . j) ) & ( for j being object st j in J holds
x . j = a . j ) ) ) )
let G be Group; for i being object st i in I holds
ex F being Group-Family of I ex h being Homomorphism of (sum F),G st
( h is bijective & F = (I --> ((1). G)) +* ({i} --> G) & ( for j being Element of I holds 1_ (F . j) = 1_ G ) & ( for x being Element of (sum F) holds h . x = x . i ) & ( for x being Element of (sum F) ex J being finite Subset of I ex a being ManySortedSet of J st
( J c= {i} & J = support (x,F) & ( support (x,F) = {} or support (x,F) = {i} ) & x = (1_ (product F)) +* a & ( for j being Element of I st j in I \ J holds
x . j = 1_ (F . j) ) & ( for j being object st j in J holds
x . j = a . j ) ) ) )
let i be object ; ( i in I implies ex F being Group-Family of I ex h being Homomorphism of (sum F),G st
( h is bijective & F = (I --> ((1). G)) +* ({i} --> G) & ( for j being Element of I holds 1_ (F . j) = 1_ G ) & ( for x being Element of (sum F) holds h . x = x . i ) & ( for x being Element of (sum F) ex J being finite Subset of I ex a being ManySortedSet of J st
( J c= {i} & J = support (x,F) & ( support (x,F) = {} or support (x,F) = {i} ) & x = (1_ (product F)) +* a & ( for j being Element of I st j in I \ J holds
x . j = 1_ (F . j) ) & ( for j being object st j in J holds
x . j = a . j ) ) ) ) )
assume A1:
i in I
; ex F being Group-Family of I ex h being Homomorphism of (sum F),G st
( h is bijective & F = (I --> ((1). G)) +* ({i} --> G) & ( for j being Element of I holds 1_ (F . j) = 1_ G ) & ( for x being Element of (sum F) holds h . x = x . i ) & ( for x being Element of (sum F) ex J being finite Subset of I ex a being ManySortedSet of J st
( J c= {i} & J = support (x,F) & ( support (x,F) = {} or support (x,F) = {i} ) & x = (1_ (product F)) +* a & ( for j being Element of I st j in I \ J holds
x . j = 1_ (F . j) ) & ( for j being object st j in J holds
x . j = a . j ) ) ) )
set v = I --> ((1). G);
set w = {i} --> G;
set F = (I --> ((1). G)) +* ({i} --> G);
A4: dom ((I --> ((1). G)) +* ({i} --> G)) =
(dom (I --> ((1). G))) \/ (dom ({i} --> G))
by FUNCT_4:def 1
.=
(dom (I --> ((1). G))) \/ {i}
by FUNCOP_1:13
.=
I \/ {i}
by FUNCOP_1:13
.=
I
by A1, XBOOLE_1:12, ZFMISC_1:31
;
A5:
i in {i}
by TARSKI:def 1;
then
i in dom ({i} --> G)
by FUNCOP_1:13;
then A7:
((I --> ((1). G)) +* ({i} --> G)) . i = ({i} --> G) . i
by FUNCT_4:13;
then A8:
((I --> ((1). G)) +* ({i} --> G)) . i = G
by A5, FUNCOP_1:7;
A9:
for j being object st j in I \ {i} holds
((I --> ((1). G)) +* ({i} --> G)) . j = (1). G
for j being object st j in I holds
((I --> ((1). G)) +* ({i} --> G)) . j is Group
then reconsider F = (I --> ((1). G)) +* ({i} --> G) as Group-Family of I by A4, Th2;
A17:
for j being Element of I holds 1_ (F . j) = 1_ G
defpred S1[ Element of (sum F), Element of G] means $2 = $1 . i;
A24:
for x being Element of (sum F) ex y being Element of G st S1[x,y]
consider h being Function of (sum F),G such that
A29:
for x being Element of (sum F) holds S1[x,h . x]
from FUNCT_2:sch 3(A24);
for y being object st y in [#] G holds
ex x being object st
( x in [#] (sum F) & y = h . x )
proof
let y be
object ;
( y in [#] G implies ex x being object st
( x in [#] (sum F) & y = h . x ) )
assume A30:
y in [#] G
;
ex x being object st
( x in [#] (sum F) & y = h . x )
reconsider i =
i as
Element of
I by A1;
set x =
(1_ (product F)) +* (
i,
y);
A32:
1_ (product F) in product F
;
A33:
y in F . i
by A5, A7, A30, FUNCOP_1:7;
then
(1_ (product F)) +* (
i,
y)
in product F
by A32, Th24;
then reconsider x =
(1_ (product F)) +* (
i,
y) as
Element of
(product F) ;
support (
x,
F)
c= {i}
by A33, Th17;
then A35:
x in sum F
by Th8;
take
x
;
( x in [#] (sum F) & y = h . x )
thus
x in [#] (sum F)
by A35;
y = h . x
A36:
dom (1_ (product F)) = I
by Th3;
reconsider x =
x as
Element of
(sum F) by A35;
reconsider y =
y as
Element of
G by A30;
S1[
x,
y]
by A36, FUNCT_7:31;
hence
y = h . x
by A29;
verum
end;
then
rng h = [#] G
by FUNCT_2:10;
then A42:
h is onto
by FUNCT_2:def 3;
A43:
for x being Element of (sum F) holds support (x,F) c= {i}
for x1, x2 being object st x1 in [#] (sum F) & x2 in [#] (sum F) & h . x1 = h . x2 holds
x1 = x2
then A62:
h is one-to-one
by FUNCT_2:19;
for x, y being Element of (sum F) holds h . (x * y) = (h . x) * (h . y)
then reconsider h = h as Homomorphism of (sum F),G by GROUP_6:def 6;
take
F
; ex h being Homomorphism of (sum F),G st
( h is bijective & F = (I --> ((1). G)) +* ({i} --> G) & ( for j being Element of I holds 1_ (F . j) = 1_ G ) & ( for x being Element of (sum F) holds h . x = x . i ) & ( for x being Element of (sum F) ex J being finite Subset of I ex a being ManySortedSet of J st
( J c= {i} & J = support (x,F) & ( support (x,F) = {} or support (x,F) = {i} ) & x = (1_ (product F)) +* a & ( for j being Element of I st j in I \ J holds
x . j = 1_ (F . j) ) & ( for j being object st j in J holds
x . j = a . j ) ) ) )
take
h
; ( h is bijective & F = (I --> ((1). G)) +* ({i} --> G) & ( for j being Element of I holds 1_ (F . j) = 1_ G ) & ( for x being Element of (sum F) holds h . x = x . i ) & ( for x being Element of (sum F) ex J being finite Subset of I ex a being ManySortedSet of J st
( J c= {i} & J = support (x,F) & ( support (x,F) = {} or support (x,F) = {i} ) & x = (1_ (product F)) +* a & ( for j being Element of I st j in I \ J holds
x . j = 1_ (F . j) ) & ( for j being object st j in J holds
x . j = a . j ) ) ) )
thus
h is bijective
by A42, A62; ( F = (I --> ((1). G)) +* ({i} --> G) & ( for j being Element of I holds 1_ (F . j) = 1_ G ) & ( for x being Element of (sum F) holds h . x = x . i ) & ( for x being Element of (sum F) ex J being finite Subset of I ex a being ManySortedSet of J st
( J c= {i} & J = support (x,F) & ( support (x,F) = {} or support (x,F) = {i} ) & x = (1_ (product F)) +* a & ( for j being Element of I st j in I \ J holds
x . j = 1_ (F . j) ) & ( for j being object st j in J holds
x . j = a . j ) ) ) )
thus
F = (I --> ((1). G)) +* ({i} --> G)
; ( ( for j being Element of I holds 1_ (F . j) = 1_ G ) & ( for x being Element of (sum F) holds h . x = x . i ) & ( for x being Element of (sum F) ex J being finite Subset of I ex a being ManySortedSet of J st
( J c= {i} & J = support (x,F) & ( support (x,F) = {} or support (x,F) = {i} ) & x = (1_ (product F)) +* a & ( for j being Element of I st j in I \ J holds
x . j = 1_ (F . j) ) & ( for j being object st j in J holds
x . j = a . j ) ) ) )
thus
for j being Element of I holds 1_ (F . j) = 1_ G
by A17; ( ( for x being Element of (sum F) holds h . x = x . i ) & ( for x being Element of (sum F) ex J being finite Subset of I ex a being ManySortedSet of J st
( J c= {i} & J = support (x,F) & ( support (x,F) = {} or support (x,F) = {i} ) & x = (1_ (product F)) +* a & ( for j being Element of I st j in I \ J holds
x . j = 1_ (F . j) ) & ( for j being object st j in J holds
x . j = a . j ) ) ) )
thus
for x being Element of (sum F) holds h . x = x . i
by A29; for x being Element of (sum F) ex J being finite Subset of I ex a being ManySortedSet of J st
( J c= {i} & J = support (x,F) & ( support (x,F) = {} or support (x,F) = {i} ) & x = (1_ (product F)) +* a & ( for j being Element of I st j in I \ J holds
x . j = 1_ (F . j) ) & ( for j being object st j in J holds
x . j = a . j ) )
let x be Element of (sum F); ex J being finite Subset of I ex a being ManySortedSet of J st
( J c= {i} & J = support (x,F) & ( support (x,F) = {} or support (x,F) = {i} ) & x = (1_ (product F)) +* a & ( for j being Element of I st j in I \ J holds
x . j = 1_ (F . j) ) & ( for j being object st j in J holds
x . j = a . j ) )
A78:
support (x,F) c= {i}
by A43;
A79:
( support (x,F) = {} or support (x,F) = {i} )
consider J being finite Subset of I, a being ManySortedSet of J such that
A85:
( J = support (x,F) & x = (1_ (product F)) +* a & ( for j being object
for G being Group st j in I \ J & G = F . j holds
x . j = 1_ G ) & ( for j being object st j in J holds
x . j = a . j ) )
by Th7;
take
J
; ex a being ManySortedSet of J st
( J c= {i} & J = support (x,F) & ( support (x,F) = {} or support (x,F) = {i} ) & x = (1_ (product F)) +* a & ( for j being Element of I st j in I \ J holds
x . j = 1_ (F . j) ) & ( for j being object st j in J holds
x . j = a . j ) )
take
a
; ( J c= {i} & J = support (x,F) & ( support (x,F) = {} or support (x,F) = {i} ) & x = (1_ (product F)) +* a & ( for j being Element of I st j in I \ J holds
x . j = 1_ (F . j) ) & ( for j being object st j in J holds
x . j = a . j ) )
thus
( J c= {i} & J = support (x,F) & ( support (x,F) = {} or support (x,F) = {i} ) & x = (1_ (product F)) +* a & ( for j being Element of I st j in I \ J holds
x . j = 1_ (F . j) ) & ( for j being object st j in J holds
x . j = a . j ) )
by A79, A85; verum