:: GROUP_12 semantic presentation

begin

registration
let I be non empty set ;
let F be Group-like multMagma-Family of I;
let i be Element of I;
clusterF . i ->  Group-like for multMagma ;
coherence
 for b1 being multMagma st b1 = F . i holds
b1 is Group-like by GROUP_7:def_6;
end;

registration
let I be non empty set ;
let F be associative multMagma-Family of I;
let i be Element of I;
clusterF . i ->  associative for multMagma ;
coherence
 for b1 being multMagma st b1 = F . i holds
b1 is associative by GROUP_7:def_7;
end;

registration
let I be non empty set ;
let F be commutative multMagma-Family of I;
let i be Element of I;
clusterF . i ->  commutative for multMagma ;
coherence
 for b1 being multMagma st b1 = F . i holds
b1 is commutative by GROUP_7:def_8;
end;


theorem Th1: :: GROUP_12:1
for I being non empty set
for F being Group-like associative multMagma-Family of I
for i being Element of I
for x being Function
for g being Element of (F . i) holds
( ( dom x = I & x . i = g & ( for j being Element of I st j <> i holds
x . j = 1_ (F . j) ) ) iff x = (1_ (product F)) +* (i,g) )
proof
let I be non empty set ; ::_thesis: for F being Group-like associative multMagma-Family of I
for i being Element of I
for x being Function
for g being Element of (F . i) holds
( ( dom x = I & x . i = g & ( for j being Element of I st j <> i holds
x . j = 1_ (F . j) ) ) iff x = (1_ (product F)) +* (i,g) )
let F be Group-like associative multMagma-Family of I; ::_thesis: for i being Element of I
for x being Function
for g being Element of (F . i) holds
( ( dom x = I & x . i = g & ( for j being Element of I st j <> i holds
x . j = 1_ (F . j) ) ) iff x = (1_ (product F)) +* (i,g) )
let i be Element of I; ::_thesis: for x being Function
for g being Element of (F . i) holds
( ( dom x = I & x . i = g & ( for j being Element of I st j <> i holds
x . j = 1_ (F . j) ) ) iff x = (1_ (product F)) +* (i,g) )
let x be Function; ::_thesis: for g being Element of (F . i) holds
( ( dom x = I & x . i = g & ( for j being Element of I st j <> i holds
x . j = 1_ (F . j) ) ) iff x = (1_ (product F)) +* (i,g) )
let g be Element of (F . i); ::_thesis: ( ( dom x = I & x . i = g & ( for j being Element of I st j <> i holds
x . j = 1_ (F . j) ) ) iff x = (1_ (product F)) +* (i,g) )
A1: now__::_thesis:_(_x_=_(1__(product_F))_+*_(i,g)_implies_(_dom_x_=_I_&_x_._i_=_g_&_(_for_j_being_Element_of_I_st_j_<>_i_holds_
x_._j_=_1__(F_._j)_)_)_)
assume A2: x = (1_ (product F)) +* (i,g) ; ::_thesis: ( dom x = I & x . i = g & ( for j being Element of I st j <> i holds
x . j = 1_ (F . j) ) )
A3: the carrier of (product F) = product (Carrier F) by GROUP_7:def_2;
thus A4: dom x = dom (1_ (product F)) by A2, FUNCT_7:30
.= I by A3, PARTFUN1:def_2 ; ::_thesis: ( x . i = g & ( for j being Element of I st j <> i holds
x . j = 1_ (F . j) ) )
 dom x = dom (1_ (product F)) by A2, FUNCT_7:30;
hence  x . i = g by A2, A4, FUNCT_7:31; ::_thesis: for j being Element of I st j <> i holds
x . j = 1_ (F . j)
thus  for j being Element of I st j <> i holds
x . j = 1_ (F . j) ::_thesis: verum
proof
let j be Element of I; ::_thesis: ( j <> i implies x . j = 1_ (F . j) )
assume  j <> i ; ::_thesis: x . j = 1_ (F . j)
then  x . j = (1_ (product F)) . j by A2, FUNCT_7:32;
hence  x . j = 1_ (F . j) by GROUP_7:6; ::_thesis: verum
end;
end;
now__::_thesis:_(_dom_x_=_I_&_x_._i_=_g_&_(_for_j_being_Element_of_I_st_j_<>_i_holds_
x_._j_=_1__(F_._j)_)_implies_x_=_(1__(product_F))_+*_(i,g)_)
assume A5: ( dom x = I & x . i = g & ( for j being Element of I st j <> i holds
x . j = 1_ (F . j) ) ) ; ::_thesis: x = (1_ (product F)) +* (i,g)
 the carrier of (product F) = product (Carrier F) by GROUP_7:def_2;
then A6: dom (1_ (product F)) = I by PARTFUN1:def_2;
A7: dom ((1_ (product F)) +* (i,g)) = dom x by A5, A6, FUNCT_7:30;
set FG = (1_ (product F)) +* (i,g);
now__::_thesis:_for_j0_being_set_st_j0_in_dom_x_holds_
x_._j0_=_((1__(product_F))_+*_(i,g))_._j0
let j0 be set ; ::_thesis: ( j0 in dom x implies x . b1 = ((1_ (product F)) +* (i,g)) . b1 )
assume  j0 in dom x ; ::_thesis: x . b1 = ((1_ (product F)) +* (i,g)) . b1
then reconsider j = j0 as Element of I by A5;
percases ( j <> i or j = i ) ;
supposeA8: j <> i ; ::_thesis: x . b1 = ((1_ (product F)) +* (i,g)) . b1
then  x . j = 1_ (F . j) by A5;
hence x . j0 = (1_ (product F)) . j by GROUP_7:6
.= ((1_ (product F)) +* (i,g)) . j0 by A8, FUNCT_7:32 ;
::_thesis: verum
end;
suppose j = i ; ::_thesis: x . b1 = ((1_ (product F)) +* (i,g)) . b1
hence  x . j0 = ((1_ (product F)) +* (i,g)) . j0 by A6, A5, FUNCT_7:31; ::_thesis: verum
end;
end;
end;
hence  x = (1_ (product F)) +* (i,g) by A7, FUNCT_1:2; ::_thesis: verum
end;
hence  ( ( dom x = I & x . i = g & ( for j being Element of I st j <> i holds
x . j = 1_ (F . j) ) ) iff x = (1_ (product F)) +* (i,g) ) by A1; ::_thesis: verum
end;

definition
let I be non empty set ;
let F be Group-like associative multMagma-Family of I;
let i be Element of I;
func ProjSet (F,i) ->  Subset of (product F) means :Def1: :: GROUP_12:def 1
 for x being set holds
( x in it iff ex g being Element of (F . i) st x = (1_ (product F)) +* (i,g) );
existence
 ex b1 being Subset of (product F) st
for x being set holds
( x in b1 iff ex g being Element of (F . i) st x = (1_ (product F)) +* (i,g) )
proof
set CF = the carrier of (product F);
defpred S1[ set ] means  ex g being Element of (F . i) st $1 = (1_ (product F)) +* (i,g);
consider H being Subset of the carrier of (product F) such that
A1: for x being set holds
( x in H iff ( x in the carrier of (product F) & S1[x] ) ) from SUBSET_1:sch_1();
take  H ; ::_thesis: for x being set holds
( x in H iff ex g being Element of (F . i) st x = (1_ (product F)) +* (i,g) )
set Gi = F . i;
A2: now__::_thesis:_for_x_being_set_st_S1[x]_holds_
x_in_the_carrier_of_(product_F)
let x be set ; ::_thesis: ( S1[x] implies x in the carrier of (product F) )
assume A3: S1[x] ; ::_thesis: x in the carrier of (product F)
A4: the carrier of (product F) = product (Carrier F) by GROUP_7:def_2;
 ex Ri being 1-sorted st
( Ri = F . i & (Carrier F) . i = the carrier of Ri ) by PRALG_1:def_13;
hence  x in the carrier of (product F) by A3, A4, YELLOW17:2; ::_thesis: verum
end;
let x be set ; ::_thesis: ( x in H iff ex g being Element of (F . i) st x = (1_ (product F)) +* (i,g) )
 ( x in H iff ( x in the carrier of (product F) & S1[x] ) ) by A1;
hence  ( x in H iff ex g being Element of (F . i) st x = (1_ (product F)) +* (i,g) ) by A2; ::_thesis: verum
end;
uniqueness
 for b1, b2 being Subset of (product F) st ( for x being set holds
( x in b1 iff ex g being Element of (F . i) st x = (1_ (product F)) +* (i,g) ) ) & ( for x being set holds
( x in b2 iff ex g being Element of (F . i) st x = (1_ (product F)) +* (i,g) ) ) holds
b1 = b2
proof
let F1, F2 be Subset of (product F); ::_thesis: ( ( for x being set holds
( x in F1 iff ex g being Element of (F . i) st x = (1_ (product F)) +* (i,g) ) ) & ( for x being set holds
( x in F2 iff ex g being Element of (F . i) st x = (1_ (product F)) +* (i,g) ) ) implies F1 = F2 )
defpred S1[ set ] means  ex g being Element of (F . i) st $1 = (1_ (product F)) +* (i,g);
assume A5: for x being set holds
( x in F1 iff S1[x] ) ; ::_thesis: ( ex x being set st
( ( x in F2 implies ex g being Element of (F . i) st x = (1_ (product F)) +* (i,g) ) implies ( ex g being Element of (F . i) st x = (1_ (product F)) +* (i,g) & not x in F2 ) ) or F1 = F2 )
assume A6: for x being set holds
( x in F2 iff S1[x] ) ; ::_thesis: F1 = F2
thus  F1 = F2 from XBOOLE_0:sch_2(A5, A6); ::_thesis: verum
end;
end;

:: deftheorem Def1 defines ProjSet GROUP_12:def_1_:_
 for I being non empty set
for F being Group-like associative multMagma-Family of I
for i being Element of I
for b4 being Subset of (product F) holds
( b4 = ProjSet (F,i) iff for x being set holds
( x in b4 iff ex g being Element of (F . i) st x = (1_ (product F)) +* (i,g) ) );

registration
let I be non empty set ;
let F be Group-like associative multMagma-Family of I;
let i be Element of I;
cluster ProjSet (F,i) ->  non empty ;
coherence
 not ProjSet (F,i) is empty
proof
set Gi = F . i;
 the carrier of (product F) = product (Carrier F) by GROUP_7:def_2;
then A1: dom (1_ (product F)) = I by PARTFUN1:def_2;
A2: dom ((1_ (product F)) +* (i,(1_ (F . i)))) = dom (1_ (product F)) by FUNCT_7:30;
set FG = (1_ (product F)) +* (i,(1_ (F . i)));
reconsider FG = (1_ (product F)) +* (i,(1_ (F . i))) as I -defined Function by A2, A1, RELAT_1:def_18;
now__::_thesis:_for_j_being_Element_of_I_holds_FG_._j_=_1__(F_._j)
let j be Element of I; ::_thesis: FG . b1 = 1_ (F . b1)
percases ( j <> i or j = i ) ;
supposeA3: j <> i ; ::_thesis: FG . b1 = 1_ (F . b1)
thus FG . j = (1_ (product F)) . j by A3, FUNCT_7:32
.= 1_ (F . j) by GROUP_7:6 ; ::_thesis: verum
end;
suppose j = i ; ::_thesis: FG . b1 = 1_ (F . b1)
hence  FG . j = 1_ (F . j) by A1, FUNCT_7:31; ::_thesis: verum
end;
end;
end;
hence  not ProjSet (F,i) is empty by Def1; ::_thesis: verum
end;
end;

theorem Th2: :: GROUP_12:2
for I being non empty set
for F being Group-like associative multMagma-Family of I
for i being Element of I
for x0 being set holds
( x0 in ProjSet (F,i) iff ex x being Function ex g being Element of (F . i) st
( x = x0 & dom x = I & x . i = g & ( for j being Element of I st j <> i holds
x . j = 1_ (F . j) ) ) )
proof
let I be non empty set ; ::_thesis: for F being Group-like associative multMagma-Family of I
for i being Element of I
for x0 being set holds
( x0 in ProjSet (F,i) iff ex x being Function ex g being Element of (F . i) st
( x = x0 & dom x = I & x . i = g & ( for j being Element of I st j <> i holds
x . j = 1_ (F . j) ) ) )
let F be Group-like associative multMagma-Family of I; ::_thesis: for i being Element of I
for x0 being set holds
( x0 in ProjSet (F,i) iff ex x being Function ex g being Element of (F . i) st
( x = x0 & dom x = I & x . i = g & ( for j being Element of I st j <> i holds
x . j = 1_ (F . j) ) ) )
let i be Element of I; ::_thesis: for x0 being set holds
( x0 in ProjSet (F,i) iff ex x being Function ex g being Element of (F . i) st
( x = x0 & dom x = I & x . i = g & ( for j being Element of I st j <> i holds
x . j = 1_ (F . j) ) ) )
let x0 be set ; ::_thesis: ( x0 in ProjSet (F,i) iff ex x being Function ex g being Element of (F . i) st
( x = x0 & dom x = I & x . i = g & ( for j being Element of I st j <> i holds
x . j = 1_ (F . j) ) ) )
defpred S1[ set ] means  ex g being Element of (F . i) st $1 = (1_ (product F)) +* (i,g);
A1: now__::_thesis:_(_x0_in_ProjSet_(F,i)_implies_ex_x_being_Function_ex_g_being_Element_of_(F_._i)_st_
(_x_=_x0_&_dom_x_=_I_&_x_._i_=_g_&_(_for_j_being_Element_of_I_st_j_<>_i_holds_
x_._j_=_1__(F_._j)_)_)_)
assume  x0 in ProjSet (F,i) ; ::_thesis: ex x being Function ex g being Element of (F . i) st
( x = x0 & dom x = I & x . i = g & ( for j being Element of I st j <> i holds
x . j = 1_ (F . j) ) )
then consider g being Element of (F . i) such that
A2: x0 = (1_ (product F)) +* (i,g) by Def1;
reconsider x = x0 as Function by A2;
take x = x; ::_thesis: ex g being Element of (F . i) st
( x = x0 & dom x = I & x . i = g & ( for j being Element of I st j <> i holds
x . j = 1_ (F . j) ) )
take g = g; ::_thesis: ( x = x0 & dom x = I & x . i = g & ( for j being Element of I st j <> i holds
x . j = 1_ (F . j) ) )
thus  x = x0 ; ::_thesis: ( dom x = I & x . i = g & ( for j being Element of I st j <> i holds
x . j = 1_ (F . j) ) )
thus  ( dom x = I & x . i = g & ( for j being Element of I st j <> i holds
x . j = 1_ (F . j) ) ) by A2, Th1; ::_thesis: verum
end;
now__::_thesis:_(_ex_x_being_Function_ex_g_being_Element_of_(F_._i)_st_
(_x_=_x0_&_dom_x_=_I_&_x_._i_=_g_&_(_for_j_being_Element_of_I_st_j_<>_i_holds_
x_._j_=_1__(F_._j)_)_)_implies_x0_in_ProjSet_(F,i)_)
assume A3: ex x being Function ex g being Element of (F . i) st
( x = x0 & dom x = I & x . i = g & ( for j being Element of I st j <> i holds
x . j = 1_ (F . j) ) ) ; ::_thesis: x0 in ProjSet (F,i)
thus  x0 in ProjSet (F,i) ::_thesis: verum
proof
consider x being Function, g being Element of (F . i) such that
A4: ( x = x0 & dom x = I & x . i = g & ( for j being Element of I st j <> i holds
x . j = 1_ (F . j) ) ) by A3;
 x = (1_ (product F)) +* (i,g) by Th1, A4;
hence  x0 in ProjSet (F,i) by Def1, A4; ::_thesis: verum
end;
end;
hence  ( x0 in ProjSet (F,i) iff ex x being Function ex g being Element of (F . i) st
( x = x0 & dom x = I & x . i = g & ( for j being Element of I st j <> i holds
x . j = 1_ (F . j) ) ) ) by A1; ::_thesis: verum
end;

theorem Th3: :: GROUP_12:3
for I being non empty set
for F being Group-like associative multMagma-Family of I
for i being Element of I
for g1, g2 being Element of (product F)
for z1, z2 being Element of (F . i) st g1 = (1_ (product F)) +* (i,z1) & g2 = (1_ (product F)) +* (i,z2) holds
g1 * g2 = (1_ (product F)) +* (i,(z1 * z2))
proof
let I be non empty set ; ::_thesis: for F being Group-like associative multMagma-Family of I
for i being Element of I
for g1, g2 being Element of (product F)
for z1, z2 being Element of (F . i) st g1 = (1_ (product F)) +* (i,z1) & g2 = (1_ (product F)) +* (i,z2) holds
g1 * g2 = (1_ (product F)) +* (i,(z1 * z2))
let F be Group-like associative multMagma-Family of I; ::_thesis: for i being Element of I
for g1, g2 being Element of (product F)
for z1, z2 being Element of (F . i) st g1 = (1_ (product F)) +* (i,z1) & g2 = (1_ (product F)) +* (i,z2) holds
g1 * g2 = (1_ (product F)) +* (i,(z1 * z2))
let i be Element of I; ::_thesis: for g1, g2 being Element of (product F)
for z1, z2 being Element of (F . i) st g1 = (1_ (product F)) +* (i,z1) & g2 = (1_ (product F)) +* (i,z2) holds
g1 * g2 = (1_ (product F)) +* (i,(z1 * z2))
let g1, g2 be Element of (product F); ::_thesis: for z1, z2 being Element of (F . i) st g1 = (1_ (product F)) +* (i,z1) & g2 = (1_ (product F)) +* (i,z2) holds
g1 * g2 = (1_ (product F)) +* (i,(z1 * z2))
let z1, z2 be Element of (F . i); ::_thesis: ( g1 = (1_ (product F)) +* (i,z1) & g2 = (1_ (product F)) +* (i,z2) implies g1 * g2 = (1_ (product F)) +* (i,(z1 * z2)) )
assume A1: ( g1 = (1_ (product F)) +* (i,z1) & g2 = (1_ (product F)) +* (i,z2) ) ; ::_thesis: g1 * g2 = (1_ (product F)) +* (i,(z1 * z2))
set x1 = g1;
set x2 = g2;
A2: ( g1 = g1 & dom g1 = I & g1 . i = z1 & ( for j being Element of I st j <> i holds
g1 . j = 1_ (F . j) ) ) by Th1, A1;
A3: ( g2 = g2 & dom g2 = I & g2 . i = z2 & ( for j being Element of I st j <> i holds
g2 . j = 1_ (F . j) ) ) by Th1, A1;
set x12 = g1 * g2;
 the carrier of (product F) = product (Carrier F) by GROUP_7:def_2;
then A4: dom (g1 * g2) = I by PARTFUN1:def_2;
A5: (g1 * g2) . i = z1 * z2 by A2, A3, GROUP_7:1;
 for j being Element of I st i <> j holds
(g1 * g2) . j = 1_ (F . j)
proof
let j be Element of I; ::_thesis: ( i <> j implies (g1 * g2) . j = 1_ (F . j) )
assume A6: i <> j ; ::_thesis: (g1 * g2) . j = 1_ (F . j)
then A7: g1 . j = 1_ (F . j) by Th1, A1;
 g2 . j = 1_ (F . j) by A6, Th1, A1;
hence (g1 * g2) . j = (1_ (F . j)) * (1_ (F . j)) by A7, GROUP_7:1
.= 1_ (F . j) by GROUP_1:def_4 ;
::_thesis: verum
end;
hence  g1 * g2 = (1_ (product F)) +* (i,(z1 * z2)) by A4, A5, Th1; ::_thesis: verum
end;

theorem Th4: :: GROUP_12:4
for I being non empty set
for F being Group-like associative multMagma-Family of I
for i being Element of I
for g1 being Element of (product F)
for z1 being Element of (F . i) st g1 = (1_ (product F)) +* (i,z1) holds
g1 " = (1_ (product F)) +* (i,(z1 "))
proof
let I be non empty set ; ::_thesis: for F being Group-like associative multMagma-Family of I
for i being Element of I
for g1 being Element of (product F)
for z1 being Element of (F . i) st g1 = (1_ (product F)) +* (i,z1) holds
g1 " = (1_ (product F)) +* (i,(z1 "))
let F be Group-like associative multMagma-Family of I; ::_thesis: for i being Element of I
for g1 being Element of (product F)
for z1 being Element of (F . i) st g1 = (1_ (product F)) +* (i,z1) holds
g1 " = (1_ (product F)) +* (i,(z1 "))
let i be Element of I; ::_thesis: for g1 being Element of (product F)
for z1 being Element of (F . i) st g1 = (1_ (product F)) +* (i,z1) holds
g1 " = (1_ (product F)) +* (i,(z1 "))
let g1 be Element of (product F); ::_thesis: for z1 being Element of (F . i) st g1 = (1_ (product F)) +* (i,z1) holds
g1 " = (1_ (product F)) +* (i,(z1 "))
let z1 be Element of (F . i); ::_thesis: ( g1 = (1_ (product F)) +* (i,z1) implies g1 " = (1_ (product F)) +* (i,(z1 ")) )
assume A1: g1 = (1_ (product F)) +* (i,z1) ; ::_thesis: g1 " = (1_ (product F)) +* (i,(z1 "))
set x1 = g1;
A2: ( g1 = g1 & dom g1 = I & g1 . i = z1 & ( for j being Element of I st j <> i holds
g1 . j = 1_ (F . j) ) ) by Th1, A1;
set x12 = g1 " ;
 the carrier of (product F) = product (Carrier F) by GROUP_7:def_2;
then A3: dom (g1 ") = I by PARTFUN1:def_2;
A4: (g1 ") . i = z1 " by A2, GROUP_7:8;
A5: for j being Element of I st i <> j holds
(g1 ") . j = 1_ (F . j)
proof
let j be Element of I; ::_thesis: ( i <> j implies (g1 ") . j = 1_ (F . j) )
assume  i <> j ; ::_thesis: (g1 ") . j = 1_ (F . j)
then  g1 . j = 1_ (F . j) by Th1, A1;
hence (g1 ") . j = (1_ (F . j)) " by GROUP_7:8
.= 1_ (F . j) by GROUP_1:8 ;
::_thesis: verum
end;
thus  g1 " = (1_ (product F)) +* (i,(z1 ")) by A3, A4, A5, Th1; ::_thesis: verum
end;

theorem Th5: :: GROUP_12:5
for I being non empty set
for F being Group-like associative multMagma-Family of I
for i being Element of I
for g1, g2 being Element of (product F) st g1 in ProjSet (F,i) & g2 in ProjSet (F,i) holds
g1 * g2 in ProjSet (F,i)
proof
let I be non empty set ; ::_thesis: for F being Group-like associative multMagma-Family of I
for i being Element of I
for g1, g2 being Element of (product F) st g1 in ProjSet (F,i) & g2 in ProjSet (F,i) holds
g1 * g2 in ProjSet (F,i)
let F be Group-like associative multMagma-Family of I; ::_thesis: for i being Element of I
for g1, g2 being Element of (product F) st g1 in ProjSet (F,i) & g2 in ProjSet (F,i) holds
g1 * g2 in ProjSet (F,i)
let i be Element of I; ::_thesis: for g1, g2 being Element of (product F) st g1 in ProjSet (F,i) & g2 in ProjSet (F,i) holds
g1 * g2 in ProjSet (F,i)
let g1, g2 be Element of (product F); ::_thesis: ( g1 in ProjSet (F,i) & g2 in ProjSet (F,i) implies g1 * g2 in ProjSet (F,i) )
assume A1: ( g1 in ProjSet (F,i) & g2 in ProjSet (F,i) ) ; ::_thesis: g1 * g2 in ProjSet (F,i)
consider z1 being Element of (F . i) such that
A2: g1 = (1_ (product F)) +* (i,z1) by Def1, A1;
consider z2 being Element of (F . i) such that
A3: g2 = (1_ (product F)) +* (i,z2) by Def1, A1;
 g1 * g2 = (1_ (product F)) +* (i,(z1 * z2)) by Th3, A2, A3;
hence  g1 * g2 in ProjSet (F,i) by Def1; ::_thesis: verum
end;

theorem Th6: :: GROUP_12:6
for I being non empty set
for F being Group-like associative multMagma-Family of I
for i being Element of I
for g being Element of (product F) st g in ProjSet (F,i) holds
g " in ProjSet (F,i)
proof
let I be non empty set ; ::_thesis: for F being Group-like associative multMagma-Family of I
for i being Element of I
for g being Element of (product F) st g in ProjSet (F,i) holds
g " in ProjSet (F,i)
let F be Group-like associative multMagma-Family of I; ::_thesis: for i being Element of I
for g being Element of (product F) st g in ProjSet (F,i) holds
g " in ProjSet (F,i)
let i be Element of I; ::_thesis: for g being Element of (product F) st g in ProjSet (F,i) holds
g " in ProjSet (F,i)
let g be Element of (product F); ::_thesis: ( g in ProjSet (F,i) implies g " in ProjSet (F,i) )
assume A1: g in ProjSet (F,i) ; ::_thesis: g " in ProjSet (F,i)
consider z being Element of (F . i) such that
A2: g = (1_ (product F)) +* (i,z) by Def1, A1;
 g " = (1_ (product F)) +* (i,(z ")) by Th4, A2;
hence  g " in ProjSet (F,i) by Def1; ::_thesis: verum
end;

definition
let I be non empty set ;
let F be Group-like associative multMagma-Family of I;
let i be Element of I;
func ProjGroup (F,i) ->  strict Subgroup of product F means :Def2: :: GROUP_12:def 2
 the carrier of it = ProjSet (F,i);
existence
 ex b1 being strict Subgroup of product F st the carrier of b1 = ProjSet (F,i)
proof
 ( ( for g1, g2 being Element of (product F) st g1 in ProjSet (F,i) & g2 in ProjSet (F,i) holds
g1 * g2 in ProjSet (F,i) ) & ( for g being Element of (product F) st g in ProjSet (F,i) holds
g " in ProjSet (F,i) ) ) by Th5, Th6;
hence  ex b1 being strict Subgroup of product F st the carrier of b1 = ProjSet (F,i) by GROUP_2:52; ::_thesis: verum
end;
uniqueness
 for b1, b2 being strict Subgroup of product F st the carrier of b1 = ProjSet (F,i) & the carrier of b2 = ProjSet (F,i) holds
b1 = b2 by GROUP_2:59;
end;

:: deftheorem Def2 defines ProjGroup GROUP_12:def_2_:_
 for I being non empty set
for F being Group-like associative multMagma-Family of I
for i being Element of I
for b4 being strict Subgroup of product F holds
( b4 = ProjGroup (F,i) iff the carrier of b4 = ProjSet (F,i) );

Lm1:  for I being non empty set
for F being Group-like associative multMagma-Family of I
for i being Element of I ex f being Homomorphism of (F . i),(ProjGroup (F,i)) st
( f is bijective & ( for x being Element of (F . i) holds f . x = (1_ (product F)) +* (i,x) ) )
proof
let I be non empty set ; ::_thesis: for F being Group-like associative multMagma-Family of I
for i being Element of I ex f being Homomorphism of (F . i),(ProjGroup (F,i)) st
( f is bijective & ( for x being Element of (F . i) holds f . x = (1_ (product F)) +* (i,x) ) )
let F be Group-like associative multMagma-Family of I; ::_thesis: for i being Element of I ex f being Homomorphism of (F . i),(ProjGroup (F,i)) st
( f is bijective & ( for x being Element of (F . i) holds f . x = (1_ (product F)) +* (i,x) ) )
let i be Element of I; ::_thesis: ex f being Homomorphism of (F . i),(ProjGroup (F,i)) st
( f is bijective & ( for x being Element of (F . i) holds f . x = (1_ (product F)) +* (i,x) ) )
A1: the carrier of (ProjGroup (F,i)) = ProjSet (F,i) by Def2;
defpred S1[ set , set ] means $2 = (1_ (product F)) +* (i,$1);
A2: for x being Element of (F . i) ex y being Element of (ProjGroup (F,i)) st S1[x,y]
proof
let x be Element of (F . i); ::_thesis: ex y being Element of (ProjGroup (F,i)) st S1[x,y]
 (1_ (product F)) +* (i,x) in ProjSet (F,i) by Def1;
hence  ex y being Element of (ProjGroup (F,i)) st S1[x,y] by A1; ::_thesis: verum
end;
consider f being Function of (F . i), the carrier of (ProjGroup (F,i)) such that
A3: for x being Element of the carrier of (F . i) holds S1[x,f . x] from FUNCT_2:sch_3(A2);
 for a, b being Element of (F . i) holds f . (a * b) = (f . a) * (f . b)
proof
let a, b be Element of (F . i); ::_thesis: f . (a * b) = (f . a) * (f . b)
A4: f . a = (1_ (product F)) +* (i,a) by A3;
A5: f . b = (1_ (product F)) +* (i,b) by A3;
A6: f . (a * b) = (1_ (product F)) +* (i,(a * b)) by A3;
 the carrier of (ProjGroup (F,i)) = ProjSet (F,i) by Def2;
then reconsider ffa = f . a, ffb = f . b as Element of (product F) by TARSKI:def_3;
thus (f . a) * (f . b) = ffa * ffb by GROUP_2:43
.= f . (a * b) by A6, A4, A5, Th3 ; ::_thesis: verum
end;
then reconsider f = f as Homomorphism of (F . i),(ProjGroup (F,i)) by GROUP_6:def_6;
take  f ; ::_thesis: ( f is bijective & ( for x being Element of (F . i) holds f . x = (1_ (product F)) +* (i,x) ) )
now__::_thesis:_for_x_being_set_st_x_in_the_carrier_of_(ProjGroup_(F,i))_holds_
x_in_rng_f
let x be set ; ::_thesis: ( x in the carrier of (ProjGroup (F,i)) implies x in rng f )
assume  x in the carrier of (ProjGroup (F,i)) ; ::_thesis: x in rng f
then consider g being Element of (F . i) such that
A7: x = (1_ (product F)) +* (i,g) by Def1, A1;
 x = f . g by A7, A3;
hence  x in rng f by FUNCT_2:4; ::_thesis: verum
end;
then A8: the carrier of (ProjGroup (F,i)) c= rng f by TARSKI:def_3;
 rng f = the carrier of (ProjGroup (F,i)) by A8, XBOOLE_0:def_10;
then A9: f is onto by FUNCT_2:def_3;
 for x1, x2 being set st x1 in the carrier of (F . i) & x2 in the carrier of (F . i) & f . x1 = f . x2 holds
x1 = x2
proof
let x1, x2 be set ; ::_thesis: ( x1 in the carrier of (F . i) & x2 in the carrier of (F . i) & f . x1 = f . x2 implies x1 = x2 )
assume A10: ( x1 in the carrier of (F . i) & x2 in the carrier of (F . i) & f . x1 = f . x2 ) ; ::_thesis: x1 = x2
then reconsider xx1 = x1, xx2 = x2 as Element of the carrier of (F . i) ;
A11: f . xx1 = (1_ (product F)) +* (i,xx1) by A3;
A12: (1_ (product F)) +* (i,xx1) = (1_ (product F)) +* (i,xx2) by A10, A11, A3;
 the carrier of (product F) = product (Carrier F) by GROUP_7:def_2;
then A13: dom (1_ (product F)) = I by PARTFUN1:def_2;
thus x1 = ((1_ (product F)) +* (i .--> xx1)) . i by FUNCT_7:94
.= ((1_ (product F)) +* (i,xx1)) . i by A13, FUNCT_7:def_3
.= ((1_ (product F)) +* (i .--> xx2)) . i by A13, A12, FUNCT_7:def_3
.= x2 by FUNCT_7:94 ; ::_thesis: verum
end;
then  f is one-to-one by FUNCT_2:19;
hence  f is bijective by A9; ::_thesis: for x being Element of (F . i) holds f . x = (1_ (product F)) +* (i,x)
thus  for x being Element of (F . i) holds f . x = (1_ (product F)) +* (i,x) by A3; ::_thesis: verum
end;

definition
let I be non empty set ;
let F be Group-like associative multMagma-Family of I;
let i be Element of I;
func 1ProdHom (F,i) ->  Homomorphism of (F . i),(ProjGroup (F,i)) means :Def3: :: GROUP_12:def 3
 for x being Element of (F . i) holds it . x = (1_ (product F)) +* (i,x);
existence
 ex b1 being Homomorphism of (F . i),(ProjGroup (F,i)) st
for x being Element of (F . i) holds b1 . x = (1_ (product F)) +* (i,x)
proof
 ex f being Homomorphism of (F . i),(ProjGroup (F,i)) st
( f is bijective & ( for x being Element of (F . i) holds f . x = (1_ (product F)) +* (i,x) ) ) by Lm1;
hence  ex b1 being Homomorphism of (F . i),(ProjGroup (F,i)) st
for x being Element of (F . i) holds b1 . x = (1_ (product F)) +* (i,x) ; ::_thesis: verum
end;
uniqueness
 for b1, b2 being Homomorphism of (F . i),(ProjGroup (F,i)) st ( for x being Element of (F . i) holds b1 . x = (1_ (product F)) +* (i,x) ) & ( for x being Element of (F . i) holds b2 . x = (1_ (product F)) +* (i,x) ) holds
b1 = b2
proof
let F1, F2 be Homomorphism of (F . i),(ProjGroup (F,i)); ::_thesis: ( ( for x being Element of (F . i) holds F1 . x = (1_ (product F)) +* (i,x) ) & ( for x being Element of (F . i) holds F2 . x = (1_ (product F)) +* (i,x) ) implies F1 = F2 )
assume that
A1: for x being Element of (F . i) holds F1 . x = (1_ (product F)) +* (i,x) and
A2: for x being Element of (F . i) holds F2 . x = (1_ (product F)) +* (i,x) ; ::_thesis: F1 = F2
now__::_thesis:_for_x_being_Element_of_(F_._i)_holds_F1_._x_=_F2_._x
let x be Element of (F . i); ::_thesis: F1 . x = F2 . x
thus F1 . x = (1_ (product F)) +* (i,x) by A1
.= F2 . x by A2 ; ::_thesis: verum
end;
hence  F1 = F2 by FUNCT_2:63; ::_thesis: verum
end;
end;

:: deftheorem Def3 defines 1ProdHom GROUP_12:def_3_:_
 for I being non empty set
for F being Group-like associative multMagma-Family of I
for i being Element of I
for b4 being Homomorphism of (F . i),(ProjGroup (F,i)) holds
( b4 = 1ProdHom (F,i) iff for x being Element of (F . i) holds b4 . x = (1_ (product F)) +* (i,x) );

registration
let I be non empty set ;
let F be Group-like associative multMagma-Family of I;
let i be Element of I;
cluster 1ProdHom (F,i) ->  bijective ;
coherence
 1ProdHom (F,i) is bijective
proof
consider f being Homomorphism of (F . i),(ProjGroup (F,i)) such that
A1: ( f is bijective & ( for x being Element of (F . i) holds f . x = (1_ (product F)) +* (i,x) ) ) by Lm1;
set F2 = 1ProdHom (F,i);
 for x being Element of (F . i) holds f . x = (1ProdHom (F,i)) . x by Def3, A1;
hence  1ProdHom (F,i) is bijective by A1, FUNCT_2:63; ::_thesis: verum
end;
end;

registration
let I be non empty set ;
let F be Group-like associative multMagma-Family of I;
let i be Element of I;
cluster ProjGroup (F,i) ->  strict normal ;
correctness
coherence
ProjGroup (F,i) is normal ;
proof
set H = ProjGroup (F,i);
set G = product F;
A1: for a being Element of (product F) holds (a * (ProjGroup (F,i))) * (a ") c= the carrier of (ProjGroup (F,i))
proof
let a be Element of (product F); ::_thesis: (a * (ProjGroup (F,i))) * (a ") c= the carrier of (ProjGroup (F,i))
now__::_thesis:_for_x_being_set_st_x_in_(a_*_(ProjGroup_(F,i)))_*_(a_")_holds_
x_in_the_carrier_of_(ProjGroup_(F,i))
let x be set ; ::_thesis: ( x in (a * (ProjGroup (F,i))) * (a ") implies x in the carrier of (ProjGroup (F,i)) )
assume  x in (a * (ProjGroup (F,i))) * (a ") ; ::_thesis: x in the carrier of (ProjGroup (F,i))
then consider h being Element of (product F) such that
A2: ( x = h * (a ") & h in a * (ProjGroup (F,i)) ) by GROUP_2:28;
consider k being Element of (product F) such that
A3: ( h = a * k & k in ProjGroup (F,i) ) by A2, GROUP_2:103;
 k in the carrier of (ProjGroup (F,i)) by A3, STRUCT_0:def_5;
then  k in ProjSet (F,i) by Def2;
then consider m being Function, g being Element of (F . i) such that
A4: ( m = k & dom m = I & m . i = g & ( for j being Element of I st j <> i holds
m . j = 1_ (F . j) ) ) by Th2;
set n = (a * k) * (a ");
A5: the carrier of (product F) = product (Carrier F) by GROUP_7:def_2;
A6: dom (Carrier F) = I by PARTFUN1:def_2;
A7: dom ((a * k) * (a ")) = I by A5, PARTFUN1:def_2;
set Gi = F . i;
consider Ri being 1-sorted  such that
A8: ( Ri = F . i & (Carrier F) . i = the carrier of Ri ) by PRALG_1:def_13;
set ak = a * k;
set ad = a " ;
reconsider xa = a . i, xk = k . i as Element of (F . i) by A8, A5, A6, CARD_3:9;
A9: (a * k) . i = xa * xk by GROUP_7:1;
A10: (a ") . i = xa " by GROUP_7:8;
A11: ((a * k) * (a ")) . i = (xa * xk) * (xa ") by A9, A10, GROUP_7:1;
now__::_thesis:_for_j_being_Element_of_I_st_j_<>_i_holds_
((a_*_k)_*_(a_"))_._j_=_1__(F_._j)
let j be Element of I; ::_thesis: ( j <> i implies ((a * k) * (a ")) . j = 1_ (F . j) )
assume  j <> i ; ::_thesis: ((a * k) * (a ")) . j = 1_ (F . j)
then A12: m . j = 1_ (F . j) by A4;
set Gj = F . j;
consider Rj being 1-sorted  such that
A13: ( Rj = F . j & (Carrier F) . j = the carrier of Rj ) by PRALG_1:def_13;
reconsider xa = a . j, xk = k . j as Element of (F . j) by A13, A5, A6, CARD_3:9;
A14: (a * k) . j = xa * xk by GROUP_7:1;
A15: (a ") . j = xa " by GROUP_7:8;
thus ((a * k) * (a ")) . j = (xa * xk) * (xa ") by A14, A15, GROUP_7:1
.= xa * (xa ") by A12, A4, GROUP_1:def_4
.= 1_ (F . j) by GROUP_1:def_5 ; ::_thesis: verum
end;
then  (a * k) * (a ") in ProjSet (F,i) by A7, A11, Th2;
hence  x in the carrier of (ProjGroup (F,i)) by Def2, A2, A3; ::_thesis: verum
end;
hence  (a * (ProjGroup (F,i))) * (a ") c= the carrier of (ProjGroup (F,i)) by TARSKI:def_3; ::_thesis: verum
end;
A16: for a being Element of (product F) holds a * (ProjGroup (F,i)) c= (ProjGroup (F,i)) * a
proof
let a be Element of (product F); ::_thesis: a * (ProjGroup (F,i)) c= (ProjGroup (F,i)) * a
A17: (a * (ProjGroup (F,i))) * (a ") c= the carrier of (ProjGroup (F,i)) by A1;
A18: (a ") * a = 1_ (product F) by GROUP_1:def_5;
((a * (ProjGroup (F,i))) * (a ")) * a = (a * ((ProjGroup (F,i)) * (a "))) * a by GROUP_2:106
.= a * (((ProjGroup (F,i)) * (a ")) * a) by GROUP_2:33
.= a * ((ProjGroup (F,i)) * ((a ") * a)) by GROUP_2:107
.= a * (ProjGroup (F,i)) by A18, GROUP_2:109 ;
hence  a * (ProjGroup (F,i)) c= (ProjGroup (F,i)) * a by A17, GROUP_3:5; ::_thesis: verum
end;
A19: for a being Element of (product F) holds (ProjGroup (F,i)) * a c= a * (ProjGroup (F,i))
proof
let a be Element of (product F); ::_thesis: (ProjGroup (F,i)) * a c= a * (ProjGroup (F,i))
A20: ((a ") * (ProjGroup (F,i))) * ((a ") ") c= the carrier of (ProjGroup (F,i)) by A1;
A21: a * (a ") = 1_ (product F) by GROUP_1:def_5;
a * (((a ") * (ProjGroup (F,i))) * a) = a * ((a ") * ((ProjGroup (F,i)) * a)) by GROUP_2:106
.= (a * (a ")) * ((ProjGroup (F,i)) * a) by GROUP_2:32
.= ((a * (a ")) * (ProjGroup (F,i))) * a by GROUP_2:106
.= (ProjGroup (F,i)) * a by A21, GROUP_2:109 ;
hence  (ProjGroup (F,i)) * a c= a * (ProjGroup (F,i)) by A20, GROUP_3:5; ::_thesis: verum
end;
 for a being Element of (product F) holds a * (ProjGroup (F,i)) = (ProjGroup (F,i)) * a
proof
let a be Element of (product F); ::_thesis: a * (ProjGroup (F,i)) = (ProjGroup (F,i)) * a
A22: a * (ProjGroup (F,i)) c= (ProjGroup (F,i)) * a by A16;
 (ProjGroup (F,i)) * a c= a * (ProjGroup (F,i)) by A19;
hence  a * (ProjGroup (F,i)) = (ProjGroup (F,i)) * a by A22, XBOOLE_0:def_10; ::_thesis: verum
end;
hence  ProjGroup (F,i) is normal by GROUP_3:117; ::_thesis: verum
end;
end;

theorem :: GROUP_12:7
for I being non empty set
for F being Group-like associative multMagma-Family of I
for i, j being Element of I
for x, y being Element of (product F) st i <> j & x in ProjGroup (F,i) & y in ProjGroup (F,j) holds
x * y = y * x
proof
let I be non empty set ; ::_thesis: for F being Group-like associative multMagma-Family of I
for i, j being Element of I
for x, y being Element of (product F) st i <> j & x in ProjGroup (F,i) & y in ProjGroup (F,j) holds
x * y = y * x
let F be Group-like associative multMagma-Family of I; ::_thesis: for i, j being Element of I
for x, y being Element of (product F) st i <> j & x in ProjGroup (F,i) & y in ProjGroup (F,j) holds
x * y = y * x
let i, j be Element of I; ::_thesis: for x, y being Element of (product F) st i <> j & x in ProjGroup (F,i) & y in ProjGroup (F,j) holds
x * y = y * x
set G = product F;
let x, y be Element of (product F); ::_thesis: ( i <> j & x in ProjGroup (F,i) & y in ProjGroup (F,j) implies x * y = y * x )
assume A1: ( i <> j & x in ProjGroup (F,i) & y in ProjGroup (F,j) ) ; ::_thesis: x * y = y * x
A2: ( the carrier of (ProjGroup (F,i)) = ProjSet (F,i) & the carrier of (ProjGroup (F,j)) = ProjSet (F,j) ) by Def2;
A3: ( x in ProjSet (F,i) & y in ProjSet (F,j) ) by A2, A1, STRUCT_0:def_5;
consider xx being Function, gx being Element of (F . i) such that
A4: ( xx = x & dom xx = I & xx . i = gx & ( for k being Element of I st k <> i holds
xx . k = 1_ (F . k) ) ) by A3, Th2;
consider yy being Function, gy being Element of (F . j) such that
A5: ( yy = y & dom yy = I & yy . j = gy & ( for k being Element of I st k <> j holds
yy . k = 1_ (F . k) ) ) by A3, Th2;
A6: the carrier of (product F) = product (Carrier F) by GROUP_7:def_2;
set xy = x * y;
set yx = y * x;
A7: dom (x * y) = I by A6, PARTFUN1:def_2;
A8: dom (y * x) = I by A6, PARTFUN1:def_2;
 for k being set st k in dom (x * y) holds
(x * y) . k = (y * x) . k
proof
let k0 be set ; ::_thesis: ( k0 in dom (x * y) implies (x * y) . k0 = (y * x) . k0 )
assume  k0 in dom (x * y) ; ::_thesis: (x * y) . k0 = (y * x) . k0
then reconsider k = k0 as Element of I by A6, PARTFUN1:def_2;
percases ( ( k0 <> i & k0 <> j ) or k0 = i or k0 = j ) ;
supposeA9: ( k0 <> i & k0 <> j ) ; ::_thesis: (x * y) . k0 = (y * x) . k0
then A10: xx . k = 1_ (F . k) by A4;
A11: yy . k = 1_ (F . k) by A9, A5;
(x * y) . k = (1_ (F . k)) * (1_ (F . k)) by A4, A5, A10, A11, GROUP_7:1
.= (y * x) . k by A4, A5, A10, A11, GROUP_7:1 ;
hence  (x * y) . k0 = (y * x) . k0 ; ::_thesis: verum
end;
supposeA12: ( k0 = i or k0 = j ) ; ::_thesis: (x * y) . k0 = (y * x) . k0
percases ( k0 = i or k0 = j ) by A12;
supposeA13: k0 = i ; ::_thesis: (x * y) . k0 = (y * x) . k0
then A14: yy . k = 1_ (F . k) by A1, A5;
reconsider gx = gx as Element of (F . k) by A13;
(x * y) . k = gx * (1_ (F . k)) by A4, A5, A14, A13, GROUP_7:1
.= gx by GROUP_1:def_4
.= (1_ (F . k)) * gx by GROUP_1:def_4
.= (y * x) . k by A4, A5, A14, A13, GROUP_7:1 ;
hence  (x * y) . k0 = (y * x) . k0 ; ::_thesis: verum
end;
supposeA15: k0 = j ; ::_thesis: (x * y) . k0 = (y * x) . k0
then A16: xx . k = 1_ (F . k) by A1, A4;
reconsider gy = gy as Element of (F . k) by A15;
(x * y) . k = (1_ (F . k)) * gy by A4, A5, A16, A15, GROUP_7:1
.= gy by GROUP_1:def_4
.= gy * (1_ (F . k)) by GROUP_1:def_4
.= (y * x) . k by A4, A5, A16, A15, GROUP_7:1 ;
hence  (x * y) . k0 = (y * x) . k0 ; ::_thesis: verum
end;
end;
end;
end;
end;
hence  x * y = y * x by A7, A8, FUNCT_1:2; ::_thesis: verum
end;

theorem Th8: :: GROUP_12:8
for n being non empty Nat
for F being Group-like associative multMagma-Family of Seg n
for J being Nat
for GJ being Group st 1 <= J & J <= n & GJ = F . J holds
for x being Element of (product F)
for s being FinSequence of (product F) st len s < J & ( for k being Element of Seg n st k in dom s holds
s . k in ProjGroup (F,k) ) & x = Product s holds
x . J = 1_ GJ
proof
let n be non empty Nat; ::_thesis: for F being Group-like associative multMagma-Family of Seg n
for J being Nat
for GJ being Group st 1 <= J & J <= n & GJ = F . J holds
for x being Element of (product F)
for s being FinSequence of (product F) st len s < J & ( for k being Element of Seg n st k in dom s holds
s . k in ProjGroup (F,k) ) & x = Product s holds
x . J = 1_ GJ
let F be Group-like associative multMagma-Family of Seg n; ::_thesis: for J being Nat
for GJ being Group st 1 <= J & J <= n & GJ = F . J holds
for x being Element of (product F)
for s being FinSequence of (product F) st len s < J & ( for k being Element of Seg n st k in dom s holds
s . k in ProjGroup (F,k) ) & x = Product s holds
x . J = 1_ GJ
let J be Nat; ::_thesis: for GJ being Group st 1 <= J & J <= n & GJ = F . J holds
for x being Element of (product F)
for s being FinSequence of (product F) st len s < J & ( for k being Element of Seg n st k in dom s holds
s . k in ProjGroup (F,k) ) & x = Product s holds
x . J = 1_ GJ
let GJ be Group; ::_thesis: ( 1 <= J & J <= n & GJ = F . J implies for x being Element of (product F)
for s being FinSequence of (product F) st len s < J & ( for k being Element of Seg n st k in dom s holds
s . k in ProjGroup (F,k) ) & x = Product s holds
x . J = 1_ GJ )
assume A1: ( 1 <= J & J <= n & GJ = F . J ) ; ::_thesis: for x being Element of (product F)
for s being FinSequence of (product F) st len s < J & ( for k being Element of Seg n st k in dom s holds
s . k in ProjGroup (F,k) ) & x = Product s holds
x . J = 1_ GJ
defpred S1[ Nat] means  for x being Element of (product F)
for s being FinSequence of (product F) st len s < J & len s = $1 & ( for k being Element of Seg n st k in dom s holds
s . k in ProjGroup (F,k) ) & x = Product s holds
x . J = 1_ GJ;
A2: S1[ 0 ]
proof
let x be Element of (product F); ::_thesis: for s being FinSequence of (product F) st len s < J & len s = 0 & ( for k being Element of Seg n st k in dom s holds
s . k in ProjGroup (F,k) ) & x = Product s holds
x . J = 1_ GJ
let s be FinSequence of (product F); ::_thesis: ( len s < J & len s = 0 & ( for k being Element of Seg n st k in dom s holds
s . k in ProjGroup (F,k) ) & x = Product s implies x . J = 1_ GJ )
assume A3: ( len s < J & len s = 0 & ( for k being Element of Seg n st k in dom s holds
s . k in ProjGroup (F,k) ) & x = Product s ) ; ::_thesis: x . J = 1_ GJ
 s = <*> the carrier of (product F) by A3;
then A4: x = 1_ (product F) by A3, GROUP_4:8;
 J in Seg n by A1, FINSEQ_1:1;
hence  x . J = 1_ GJ by A1, A4, GROUP_7:6; ::_thesis: verum
end;
A5: for m being Element of NAT st S1[m] holds
S1[m + 1]
proof
let m be Element of NAT ; ::_thesis: ( S1[m] implies S1[m + 1] )
assume A6: S1[m] ; ::_thesis: S1[m + 1]
let x be Element of (product F); ::_thesis: for s being FinSequence of (product F) st len s < J & len s = m + 1 & ( for k being Element of Seg n st k in dom s holds
s . k in ProjGroup (F,k) ) & x = Product s holds
x . J = 1_ GJ
let s be FinSequence of (product F); ::_thesis: ( len s < J & len s = m + 1 & ( for k being Element of Seg n st k in dom s holds
s . k in ProjGroup (F,k) ) & x = Product s implies x . J = 1_ GJ )
assume A7: ( len s < J & len s = m + 1 & ( for k being Element of Seg n st k in dom s holds
s . k in ProjGroup (F,k) ) & x = Product s ) ; ::_thesis: x . J = 1_ GJ
A8: m < m + 1 by NAT_1:13;
A9: 1 <= len s by A7, NAT_1:11;
 ( 1 <= len s & len s <= n ) by A7, A1, NAT_1:11, XXREAL_0:2;
then  len s in Seg n ;
then reconsider ls = len s as Element of Seg n ;
set t = s | m;
A10: now__::_thesis:_for_k_being_Element_of_Seg_n_st_k_in_dom_(s_|_m)_holds_
(s_|_m)_._k_in_ProjGroup_(F,k)
let k be Element of Seg n; ::_thesis: ( k in dom (s | m) implies (s | m) . k in ProjGroup (F,k) )
assume A11: k in dom (s | m) ; ::_thesis: (s | m) . k in ProjGroup (F,k)
A12: (s | m) . k = s . k by A11, FUNCT_1:47;
 k in dom s by A11, RELAT_1:57;
hence  (s | m) . k in ProjGroup (F,k) by A12, A7; ::_thesis: verum
end;
set y = Product (s | m);
 dom s = Seg (m + 1) by A7, FINSEQ_1:def_3;
then  Seg m c= dom s by A8, FINSEQ_1:5;
then A13: dom (s | m) = Seg m by RELAT_1:62;
then A14: len (s | m) = m by FINSEQ_1:def_3;
A15: len (s | m) = (len s) - 1 by A13, A7, FINSEQ_1:def_3;
A16: (Product (s | m)) . J = 1_ GJ by A6, A10, A15, A7, XREAL_1:51;
 len s in Seg (len s) by A9;
then A17: len s in dom s by FINSEQ_1:def_3;
then reconsider sn = s . (len s) as Element of (product F) by FINSEQ_2:11;
A18: (len (s | m)) + 1 = len s by A13, A7, FINSEQ_1:def_3;
 len ((s | m) ^ <*sn*>) = len s by A18, FINSEQ_2:16;
then A19: dom ((s | m) ^ <*sn*>) = Seg (len s) by FINSEQ_1:def_3
.= dom s by FINSEQ_1:def_3 ;
A20: s = (s | m) ^ <*sn*>
proof
 for k being Nat st k in dom s holds
s . k = ((s | m) ^ <*sn*>) . k
proof
let k be Nat; ::_thesis: ( k in dom s implies s . k = ((s | m) ^ <*sn*>) . k )
assume  k in dom s ; ::_thesis: s . k = ((s | m) ^ <*sn*>) . k
then A21: k in Seg ((len (s | m)) + 1) by A18, FINSEQ_1:def_3;
now__::_thesis:_(_(_k_in_Seg_(len_(s_|_m))_&_s_._k_=_((s_|_m)_^_<*sn*>)_._k_)_or_(_k_=_(len_(s_|_m))_+_1_&_s_._k_=_((s_|_m)_^_<*sn*>)_._k_)_)
percases ( k in Seg (len (s | m)) or k = (len (s | m)) + 1 ) by A21, FINSEQ_2:7;
caseA22: k in Seg (len (s | m)) ; ::_thesis: s . k = ((s | m) ^ <*sn*>) . k
then  k in dom (s | m) by FINSEQ_1:def_3;
then ((s | m) ^ <*sn*>) . k = (s | m) . k by FINSEQ_1:def_7
.= s . k by A22, A14, FUNCT_1:49 ;
hence  s . k = ((s | m) ^ <*sn*>) . k ; ::_thesis: verum
end;
case k = (len (s | m)) + 1 ; ::_thesis: s . k = ((s | m) ^ <*sn*>) . k
hence  s . k = ((s | m) ^ <*sn*>) . k by A18, FINSEQ_1:42; ::_thesis: verum
end;
end;
end;
hence  s . k = ((s | m) ^ <*sn*>) . k ; ::_thesis: verum
end;
hence  s = (s | m) ^ <*sn*> by A19, FINSEQ_1:13; ::_thesis: verum
end;
A23: x = (Product (s | m)) * sn by A20, A7, GROUP_4:6;
 s . (len s) in ProjGroup (F,ls) by A7, A17;
then  s . (len s) in the carrier of (ProjGroup (F,ls)) by STRUCT_0:def_5;
then A24: s . (len s) in ProjSet (F,ls) by Def2;
consider snn being Function, gn being Element of (F . ls) such that
A25: ( snn = sn & dom snn = Seg n & snn . ls = gn & ( for k being Element of Seg n st k <> ls holds
snn . k = 1_ (F . k) ) ) by A24, Th2;
thus  x . J = 1_ GJ ::_thesis: verum
proof
reconsider J0 = J as Element of Seg n by A1, FINSEQ_1:1;
A26: snn . J0 = 1_ (F . J0) by A25, A7;
thus x . J = (1_ (F . J0)) * (1_ (F . J0)) by A16, A25, A26, A23, A1, GROUP_7:1
.= 1_ GJ by A1, GROUP_1:def_4 ; ::_thesis: verum
end;
end;
 for m being Element of NAT holds S1[m] from NAT_1:sch_1(A2, A5);
hence  for x being Element of (product F)
for s being FinSequence of (product F) st len s < J & ( for k being Element of Seg n st k in dom s holds
s . k in ProjGroup (F,k) ) & x = Product s holds
x . J = 1_ GJ ; ::_thesis: verum
end;

theorem Th9: :: GROUP_12:9
for n being non empty Nat
for F being Group-like associative multMagma-Family of Seg n
for x being Element of (product F)
for s being FinSequence of (product F) st len s = n & ( for k being Element of Seg n holds s . k in ProjGroup (F,k) ) & x = Product s holds
for i being Nat st 1 <= i & i <= n holds
ex si being Element of (product F) st
( si = s . i & x . i = si . i )
proof
let n be non empty Nat; ::_thesis: for F being Group-like associative multMagma-Family of Seg n
for x being Element of (product F)
for s being FinSequence of (product F) st len s = n & ( for k being Element of Seg n holds s . k in ProjGroup (F,k) ) & x = Product s holds
for i being Nat st 1 <= i & i <= n holds
ex si being Element of (product F) st
( si = s . i & x . i = si . i )
let F be Group-like associative multMagma-Family of Seg n; ::_thesis: for x being Element of (product F)
for s being FinSequence of (product F) st len s = n & ( for k being Element of Seg n holds s . k in ProjGroup (F,k) ) & x = Product s holds
for i being Nat st 1 <= i & i <= n holds
ex si being Element of (product F) st
( si = s . i & x . i = si . i )
defpred S1[ Nat] means  for x being Element of (product F)
for s being FinSequence of (product F) st 1 <= len s & len s <= $1 & $1 <= n & ( for k being Element of Seg n st k in dom s holds
s . k in ProjGroup (F,k) ) & x = Product s holds
for i being Nat st 1 <= i & i <= len s holds
ex si being Element of (product F) st
( si = s . i & x . i = si . i );
A1: S1[ 0 ] ;
A2: for m being Element of NAT st S1[m] holds
S1[m + 1]
proof
let m be Element of NAT ; ::_thesis: ( S1[m] implies S1[m + 1] )
assume A3: S1[m] ; ::_thesis: S1[m + 1]
let x be Element of (product F); ::_thesis: for s being FinSequence of (product F) st 1 <= len s & len s <= m + 1 & m + 1 <= n & ( for k being Element of Seg n st k in dom s holds
s . k in ProjGroup (F,k) ) & x = Product s holds
for i being Nat st 1 <= i & i <= len s holds
ex si being Element of (product F) st
( si = s . i & x . i = si . i )
let s be FinSequence of (product F); ::_thesis: ( 1 <= len s & len s <= m + 1 & m + 1 <= n & ( for k being Element of Seg n st k in dom s holds
s . k in ProjGroup (F,k) ) & x = Product s implies for i being Nat st 1 <= i & i <= len s holds
ex si being Element of (product F) st
( si = s . i & x . i = si . i ) )
assume A4: ( 1 <= len s & len s <= m + 1 & m + 1 <= n & ( for k being Element of Seg n st k in dom s holds
s . k in ProjGroup (F,k) ) & x = Product s ) ; ::_thesis: for i being Nat st 1 <= i & i <= len s holds
ex si being Element of (product F) st
( si = s . i & x . i = si . i )
percases ( m = 0 or m <> 0 ) ;
suppose m = 0 ; ::_thesis: for i being Nat st 1 <= i & i <= len s holds
ex si being Element of (product F) st
( si = s . i & x . i = si . i )
then A5: len s = 1 by A4, XXREAL_0:1;
then A6: s = <*(s . 1)*> by FINSEQ_1:40;
thus  for i being Nat st 1 <= i & i <= len s holds
ex si being Element of (product F) st
( si = s . i & x . i = si . i ) ::_thesis: verum
proof
let i be Nat; ::_thesis: ( 1 <= i & i <= len s implies ex si being Element of (product F) st
( si = s . i & x . i = si . i ) )
assume A7: ( 1 <= i & i <= len s ) ; ::_thesis: ex si being Element of (product F) st
( si = s . i & x . i = si . i )
 1 in Seg (len s) by A4;
then  1 in dom s by FINSEQ_1:def_3;
then reconsider si = s . 1 as Element of (product F) by FINSEQ_2:11;
take  si ; ::_thesis: ( si = s . i & x . i = si . i )
thus  ( si = s . i & x . i = si . i ) by A7, A6, A4, A5, GROUP_4:9, XXREAL_0:1; ::_thesis: verum
end;
end;
supposeA8: m <> 0 ; ::_thesis: for i being Nat st 1 <= i & i <= len s holds
ex si being Element of (product F) st
( si = s . i & x . i = si . i )
now__::_thesis:_for_i_being_Nat_st_1_<=_i_&_i_<=_len_s_holds_
ex_si_being_Element_of_(product_F)_st_
(_si_=_s_._i_&_x_._i_=_si_._i_)
percases ( len s <= m or len s > m ) ;
supposeA9: len s <= m ; ::_thesis: for i being Nat st 1 <= i & i <= len s holds
ex si being Element of (product F) st
( si = s . i & x . i = si . i )
 ( 1 <= len s & len s <= m & m <= n )
proof
 (m + 1) - 1 <= n - 0 by A4, XREAL_1:13;
hence  ( 1 <= len s & len s <= m & m <= n ) by A4, A9; ::_thesis: verum
end;
hence  for i being Nat st 1 <= i & i <= len s holds
ex si being Element of (product F) st
( si = s . i & x . i = si . i ) by A3, A4; ::_thesis: verum
end;
supposeA10: len s > m ; ::_thesis: for i being Nat st 1 <= i & i <= len s holds
ex si being Element of (product F) st
( si = s . i & x . i = si . i )
A11: len s = m + 1 by A4, A10, NAT_1:8;
A12: len s <= n by A4, A10, NAT_1:8;
then  len s in Seg n by A4;
then reconsider ls = len s as Element of Seg n ;
set t = s | m;
A13: m < m + 1 by NAT_1:13;
 dom s = Seg (m + 1) by A11, FINSEQ_1:def_3;
then  Seg m c= dom s by A13, FINSEQ_1:5;
then  dom (s | m) = Seg m by RELAT_1:62;
then A14: len (s | m) = m by FINSEQ_1:def_3;
A15: 0 + 1 <= m by A8, NAT_1:13;
A16: (m + 1) - 1 <= n - 0 by A4, XREAL_1:13;
A17: ( dom s = Seg (len s) & dom (s | m) = Seg (len (s | m)) ) by FINSEQ_1:def_3;
A18: now__::_thesis:_for_k_being_Element_of_Seg_n_st_k_in_dom_(s_|_m)_holds_
(s_|_m)_._k_in_ProjGroup_(F,k)
let k be Element of Seg n; ::_thesis: ( k in dom (s | m) implies (s | m) . k in ProjGroup (F,k) )
assume A19: k in dom (s | m) ; ::_thesis: (s | m) . k in ProjGroup (F,k)
then A20: (s | m) . k = s . k by FUNCT_1:47;
 Seg (len (s | m)) c= Seg (len s) by A14, A10, FINSEQ_1:5;
hence  (s | m) . k in ProjGroup (F,k) by A20, A4, A19, A17; ::_thesis: verum
end;
set y = Product (s | m);
A21: len s in Seg (len s) by A4;
then reconsider sn = s . (len s) as Element of (product F) by A17, FINSEQ_2:11;
A22: s = (s | m) ^ <*sn*> by A11, FINSEQ_3:55;
A23: x = (Product (s | m)) * sn by A22, A4, GROUP_4:6;
 s . (len s) in ProjGroup (F,ls) by A17, A4, A21;
then  s . (len s) in the carrier of (ProjGroup (F,ls)) by STRUCT_0:def_5;
then A24: s . (len s) in ProjSet (F,ls) by Def2;
set Gn = F . ls;
consider snn being Function, gn being Element of (F . ls) such that
A25: ( snn = sn & dom snn = Seg n & snn . ls = gn & ( for k being Element of Seg n st k <> ls holds
snn . k = 1_ (F . k) ) ) by A24, Th2;
thus  for i being Nat st 1 <= i & i <= len s holds
ex si being Element of (product F) st
( si = s . i & x . i = si . i ) ::_thesis: verum
proof
let i be Nat; ::_thesis: ( 1 <= i & i <= len s implies ex si being Element of (product F) st
( si = s . i & x . i = si . i ) )
assume A26: ( 1 <= i & i <= len s ) ; ::_thesis: ex si being Element of (product F) st
( si = s . i & x . i = si . i )
percases ( i <> len s or i = len s ) ;
supposeA27: i <> len s ; ::_thesis: ex si being Element of (product F) st
( si = s . i & x . i = si . i )
then A28: i < len s by A26, XXREAL_0:1;
len s = (len (s | m)) + (len <*sn*>) by A22, FINSEQ_1:22
.= (len (s | m)) + 1 by FINSEQ_1:40 ;
then A29: ( 1 <= i & i <= len (s | m) ) by A26, A28, NAT_1:13;
then consider ti being Element of (product F) such that
A30: ( ti = (s | m) . i & (Product (s | m)) . i = ti . i ) by A3, A16, A18, A14, A15;
A31: (s | m) . i = s . i by A29, A22, FINSEQ_1:64;
 ( 1 <= i & i <= n ) by A29, A16, A14, XXREAL_0:2;
then reconsider ii = i as Element of Seg n by FINSEQ_1:1;
A32: sn . ii = 1_ (F . ii) by A25, A27;
consider Rii being 1-sorted  such that
A33: ( Rii = F . ii & (Carrier F) . ii = the carrier of Rii ) by PRALG_1:def_13;
A34: the carrier of (product F) = product (Carrier F) by GROUP_7:def_2;
A35: dom (Carrier F) = Seg n by PARTFUN1:def_2;
reconsider tii = ti . i as Element of (F . ii) by A33, A34, A35, CARD_3:9;
x . i = tii * (1_ (F . ii)) by A30, A32, A23, GROUP_7:1
.= ti . i by GROUP_1:def_4 ;
hence  ex si being Element of (product F) st
( si = s . i & x . i = si . i ) by A30, A31; ::_thesis: verum
end;
supposeA36: i = len s ; ::_thesis: ex si being Element of (product F) st
( si = s . i & x . i = si . i )
A37: (Product (s | m)) . i = 1_ (F . ls) by A36, Th8, A18, A10, A14, A12, A26;
x . i = (1_ (F . ls)) * gn by A36, A37, A25, A23, GROUP_7:1
.= sn . i by A25, A36, GROUP_1:def_4 ;
hence  ex si being Element of (product F) st
( si = s . i & x . i = si . i ) by A36; ::_thesis: verum
end;
end;
end;
end;
end;
end;
hence  for i being Nat st 1 <= i & i <= len s holds
ex si being Element of (product F) st
( si = s . i & x . i = si . i ) ; ::_thesis: verum
end;
end;
end;
A38: for m being Element of NAT holds S1[m] from NAT_1:sch_1(A1, A2);
thus  for x being Element of (product F)
for s being FinSequence of (product F) st len s = n & ( for k being Element of Seg n holds s . k in ProjGroup (F,k) ) & x = Product s holds
for i being Nat st 1 <= i & i <= n holds
ex si being Element of (product F) st
( si = s . i & x . i = si . i ) ::_thesis: verum
proof
let x be Element of (product F); ::_thesis: for s being FinSequence of (product F) st len s = n & ( for k being Element of Seg n holds s . k in ProjGroup (F,k) ) & x = Product s holds
for i being Nat st 1 <= i & i <= n holds
ex si being Element of (product F) st
( si = s . i & x . i = si . i )
let s be FinSequence of (product F); ::_thesis: ( len s = n & ( for k being Element of Seg n holds s . k in ProjGroup (F,k) ) & x = Product s implies for i being Nat st 1 <= i & i <= n holds
ex si being Element of (product F) st
( si = s . i & x . i = si . i ) )
assume A39: ( len s = n & ( for k being Element of Seg n holds s . k in ProjGroup (F,k) ) & x = Product s ) ; ::_thesis: for i being Nat st 1 <= i & i <= n holds
ex si being Element of (product F) st
( si = s . i & x . i = si . i )
A40: ( 1 <= len s & len s <= n ) by A39, NAT_1:14;
 for k being Element of Seg n st k in dom s holds
s . k in ProjGroup (F,k) by A39;
hence  for i being Nat st 1 <= i & i <= n holds
ex si being Element of (product F) st
( si = s . i & x . i = si . i ) by A39, A40, A38; ::_thesis: verum
end;
end;

theorem Th10: :: GROUP_12:10
for n being non empty Nat
for F being Group-like associative multMagma-Family of Seg n
for x being Element of (product F)
for s, t being FinSequence of (product F) st len s = n & ( for k being Element of Seg n holds s . k in ProjGroup (F,k) ) & x = Product s & len t = n & ( for k being Element of Seg n holds t . k in ProjGroup (F,k) ) & x = Product t holds
s = t
proof
let n be non empty Nat; ::_thesis: for F being Group-like associative multMagma-Family of Seg n
for x being Element of (product F)
for s, t being FinSequence of (product F) st len s = n & ( for k being Element of Seg n holds s . k in ProjGroup (F,k) ) & x = Product s & len t = n & ( for k being Element of Seg n holds t . k in ProjGroup (F,k) ) & x = Product t holds
s = t
let F be Group-like associative multMagma-Family of Seg n; ::_thesis: for x being Element of (product F)
for s, t being FinSequence of (product F) st len s = n & ( for k being Element of Seg n holds s . k in ProjGroup (F,k) ) & x = Product s & len t = n & ( for k being Element of Seg n holds t . k in ProjGroup (F,k) ) & x = Product t holds
s = t
let x be Element of (product F); ::_thesis: for s, t being FinSequence of (product F) st len s = n & ( for k being Element of Seg n holds s . k in ProjGroup (F,k) ) & x = Product s & len t = n & ( for k being Element of Seg n holds t . k in ProjGroup (F,k) ) & x = Product t holds
s = t
let s, t be FinSequence of (product F); ::_thesis: ( len s = n & ( for k being Element of Seg n holds s . k in ProjGroup (F,k) ) & x = Product s & len t = n & ( for k being Element of Seg n holds t . k in ProjGroup (F,k) ) & x = Product t implies s = t )
set I = Seg n;
assume that
A1: len s = n and
A2: for k being Element of Seg n holds s . k in ProjGroup (F,k) and
A3: x = Product s and
A4: len t = n and
A5: for k being Element of Seg n holds t . k in ProjGroup (F,k) and
A6: x = Product t ; ::_thesis: s = t
now__::_thesis:_for_i_being_Nat_st_1_<=_i_&_i_<=_n_holds_
s_._i_=_t_._i
let i be Nat; ::_thesis: ( 1 <= i & i <= n implies s . i = t . i )
assume A7: ( 1 <= i & i <= n ) ; ::_thesis: s . i = t . i
then reconsider i0 = i as Element of Seg n by FINSEQ_1:1;
consider si being Element of (product F) such that
A8: ( si = s . i & x . i = si . i ) by A1, A2, A3, A7, Th9;
consider ti being Element of (product F) such that
A9: ( ti = t . i & x . i = ti . i ) by A4, A5, A6, A7, Th9;
 s . i0 in ProjGroup (F,i0) by A2;
then  s . i0 in the carrier of (ProjGroup (F,i0)) by STRUCT_0:def_5;
then A10: s . i0 in ProjSet (F,i0) by Def2;
consider sn being Function, gn being Element of (F . i0) such that
A11: ( sn = si & dom sn = Seg n & sn . i0 = gn & ( for k being Element of Seg n st k <> i0 holds
sn . k = 1_ (F . k) ) ) by A8, A10, Th2;
 t . i0 in ProjGroup (F,i0) by A5;
then  t . i0 in the carrier of (ProjGroup (F,i0)) by STRUCT_0:def_5;
then A12: t . i0 in ProjSet (F,i0) by Def2;
consider tn being Function, fn being Element of (F . i0) such that
A13: ( tn = ti & dom tn = Seg n & tn . i0 = fn & ( for k being Element of Seg n st k <> i0 holds
tn . k = 1_ (F . k) ) ) by A9, A12, Th2;
now__::_thesis:_for_x_being_set_st_x_in_dom_sn_holds_
sn_._x_=_tn_._x
let x be set ; ::_thesis: ( x in dom sn implies sn . b1 = tn . b1 )
assume  x in dom sn ; ::_thesis: sn . b1 = tn . b1
then reconsider j = x as Element of Seg n by A11;
percases ( j = i or j <> i ) ;
suppose j = i ; ::_thesis: sn . b1 = tn . b1
hence  sn . x = tn . x by A8, A9, A11, A13; ::_thesis: verum
end;
supposeA14: j <> i ; ::_thesis: sn . b1 = tn . b1
then  sn . j = 1_ (F . j) by A11;
hence  sn . x = tn . x by A14, A13; ::_thesis: verum
end;
end;
end;
hence  s . i = t . i by A8, A9, A11, A13, FUNCT_1:2; ::_thesis: verum
end;
hence  s = t by A1, A4, FINSEQ_1:14; ::_thesis: verum
end;

theorem Th11: :: GROUP_12:11
for n being non empty Nat
for F being Group-like associative multMagma-Family of Seg n
for x being Element of (product F) ex s being FinSequence of (product F) st
( len s = n & ( for k being Element of Seg n holds s . k in ProjGroup (F,k) ) & x = Product s )
proof
let n be non empty Nat; ::_thesis: for F being Group-like associative multMagma-Family of Seg n
for x being Element of (product F) ex s being FinSequence of (product F) st
( len s = n & ( for k being Element of Seg n holds s . k in ProjGroup (F,k) ) & x = Product s )
let F be Group-like associative multMagma-Family of Seg n; ::_thesis: for x being Element of (product F) ex s being FinSequence of (product F) st
( len s = n & ( for k being Element of Seg n holds s . k in ProjGroup (F,k) ) & x = Product s )
let x be Element of (product F); ::_thesis: ex s being FinSequence of (product F) st
( len s = n & ( for k being Element of Seg n holds s . k in ProjGroup (F,k) ) & x = Product s )
set I = Seg n;
defpred S1[ Nat, set ] means  ex k being Element of Seg n ex g being Element of (F . k) st
( k = $1 & x . k = g & $2 = (1_ (product F)) +* (k,g) );
A1: for k being Nat st k in Seg n holds
ex z being Element of (product F) st S1[k,z]
proof
let k be Nat; ::_thesis: ( k in Seg n implies ex z being Element of (product F) st S1[k,z] )
assume  k in Seg n ; ::_thesis: ex z being Element of (product F) st S1[k,z]
then reconsider k0 = k as Element of Seg n ;
A2: the carrier of (product F) = product (Carrier F) by GROUP_7:def_2;
A3: dom (Carrier F) = Seg n by PARTFUN1:def_2;
consider Rj being 1-sorted  such that
A4: ( Rj = F . k0 & (Carrier F) . k0 = the carrier of Rj ) by PRALG_1:def_13;
reconsider g = x . k0 as Element of (F . k0) by A4, A3, A2, CARD_3:9;
 (1_ (product F)) +* (k0,g) in ProjSet (F,k0) by Def1;
then reconsider z = (1_ (product F)) +* (k0,g) as Element of (product F) ;
take  z ; ::_thesis: S1[k,z]
thus  S1[k,z] ; ::_thesis: verum
end;
consider s being FinSequence of (product F) such that
A5: ( dom s = Seg n & ( for k being Nat st k in Seg n holds
S1[k,s . k] ) ) from FINSEQ_1:sch_5(A1);
take  s ; ::_thesis: ( len s = n & ( for k being Element of Seg n holds s . k in ProjGroup (F,k) ) & x = Product s )
 n in NAT by ORDINAL1:def_12;
hence A6: len s = n by A5, FINSEQ_1:def_3; ::_thesis: ( ( for k being Element of Seg n holds s . k in ProjGroup (F,k) ) & x = Product s )
thus A7: for k being Element of Seg n holds s . k in ProjGroup (F,k) ::_thesis: x = Product s
proof
let k be Element of Seg n; ::_thesis: s . k in ProjGroup (F,k)
 ex k0 being Element of Seg n ex g being Element of (F . k0) st
( k0 = k & x . k0 = g & s . k = (1_ (product F)) +* (k0,g) ) by A5;
then A8: s . k in ProjSet (F,k) by Def1;
 the carrier of (ProjGroup (F,k)) = ProjSet (F,k) by Def2;
hence  s . k in ProjGroup (F,k) by A8, STRUCT_0:def_5; ::_thesis: verum
end;
set y = Product s;
A9: the carrier of (product F) = product (Carrier F) by GROUP_7:def_2;
A10: dom x = Seg n by A9, PARTFUN1:def_2;
A11: dom (Product s) = Seg n by A9, PARTFUN1:def_2;
A12: dom (1_ (product F)) = Seg n by A9, PARTFUN1:def_2;
now__::_thesis:_for_t_being_set_st_t_in_dom_x_holds_
x_._t_=_(Product_s)_._t
let t be set ; ::_thesis: ( t in dom x implies x . t = (Product s) . t )
assume  t in dom x ; ::_thesis: x . t = (Product s) . t
then A13: t in Seg n by A9, PARTFUN1:def_2;
then reconsider i = t as Nat ;
 ( 1 <= i & i <= n ) by A13, FINSEQ_1:1;
then A14: ex si being Element of (product F) st
( si = s . i & (Product s) . i = si . i ) by Th9, A6, A7;
 ex i1 being Element of Seg n ex g being Element of (F . i1) st
( i1 = i & x . i1 = g & s . i = (1_ (product F)) +* (i1,g) ) by A13, A5;
hence  x . t = (Product s) . t by A12, A14, FUNCT_7:31; ::_thesis: verum
end;
hence  x = Product s by A10, A11, FUNCT_1:2; ::_thesis: verum
end;

theorem Th12: :: GROUP_12:12
for n being non empty Nat
for G being commutative Group
for F being Group-like associative multMagma-Family of Seg n st ( for i being Element of Seg n holds F . i is Subgroup of G ) & ( for x being Element of G ex s being FinSequence of G st
( len s = n & ( for k being Element of Seg n holds s . k in F . k ) & x = Product s ) ) & ( for s, t being FinSequence of G st len s = n & ( for k being Element of Seg n holds s . k in F . k ) & len t = n & ( for k being Element of Seg n holds t . k in F . k ) & Product s = Product t holds
s = t ) holds
ex f being Homomorphism of (product F),G st
( f is bijective & ( for x being Element of (product F) ex s being FinSequence of G st
( len s = n & ( for k being Element of Seg n holds s . k in F . k ) & s = x & f . x = Product s ) ) )
proof
let n be non empty Nat; ::_thesis: for G being commutative Group
for F being Group-like associative multMagma-Family of Seg n st ( for i being Element of Seg n holds F . i is Subgroup of G ) & ( for x being Element of G ex s being FinSequence of G st
( len s = n & ( for k being Element of Seg n holds s . k in F . k ) & x = Product s ) ) & ( for s, t being FinSequence of G st len s = n & ( for k being Element of Seg n holds s . k in F . k ) & len t = n & ( for k being Element of Seg n holds t . k in F . k ) & Product s = Product t holds
s = t ) holds
ex f being Homomorphism of (product F),G st
( f is bijective & ( for x being Element of (product F) ex s being FinSequence of G st
( len s = n & ( for k being Element of Seg n holds s . k in F . k ) & s = x & f . x = Product s ) ) )
let G be commutative Group; ::_thesis: for F being Group-like associative multMagma-Family of Seg n st ( for i being Element of Seg n holds F . i is Subgroup of G ) & ( for x being Element of G ex s being FinSequence of G st
( len s = n & ( for k being Element of Seg n holds s . k in F . k ) & x = Product s ) ) & ( for s, t being FinSequence of G st len s = n & ( for k being Element of Seg n holds s . k in F . k ) & len t = n & ( for k being Element of Seg n holds t . k in F . k ) & Product s = Product t holds
s = t ) holds
ex f being Homomorphism of (product F),G st
( f is bijective & ( for x being Element of (product F) ex s being FinSequence of G st
( len s = n & ( for k being Element of Seg n holds s . k in F . k ) & s = x & f . x = Product s ) ) )
let F be Group-like associative multMagma-Family of Seg n; ::_thesis: ( ( for i being Element of Seg n holds F . i is Subgroup of G ) & ( for x being Element of G ex s being FinSequence of G st
( len s = n & ( for k being Element of Seg n holds s . k in F . k ) & x = Product s ) ) & ( for s, t being FinSequence of G st len s = n & ( for k being Element of Seg n holds s . k in F . k ) & len t = n & ( for k being Element of Seg n holds t . k in F . k ) & Product s = Product t holds
s = t ) implies ex f being Homomorphism of (product F),G st
( f is bijective & ( for x being Element of (product F) ex s being FinSequence of G st
( len s = n & ( for k being Element of Seg n holds s . k in F . k ) & s = x & f . x = Product s ) ) ) )
set I = Seg n;
assume that
A1: for i being Element of Seg n holds F . i is Subgroup of G and
A2: for x being Element of G ex s being FinSequence of G st
( len s = n & ( for k being Element of Seg n holds s . k in F . k ) & x = Product s ) and
A3: for s, t being FinSequence of G st len s = n & ( for k being Element of Seg n holds s . k in F . k ) & len t = n & ( for k being Element of Seg n holds t . k in F . k ) & Product s = Product t holds
s = t ; ::_thesis: ex f being Homomorphism of (product F),G st
( f is bijective & ( for x being Element of (product F) ex s being FinSequence of G st
( len s = n & ( for k being Element of Seg n holds s . k in F . k ) & s = x & f . x = Product s ) ) )
A4: for x being Element of (product F) holds
( x is FinSequence of G & dom x = Seg n & dom x = dom (Carrier F) & ( for i being set st i in dom (Carrier F) holds
x . i in (Carrier F) . i ) )
proof
let x be Element of (product F); ::_thesis: ( x is FinSequence of G & dom x = Seg n & dom x = dom (Carrier F) & ( for i being set st i in dom (Carrier F) holds
x . i in (Carrier F) . i ) )
A5: the carrier of (product F) = product (Carrier F) by GROUP_7:def_2;
A6: dom (Carrier F) = Seg n by PARTFUN1:def_2;
 dom x = Seg n by A5, PARTFUN1:def_2;
then reconsider s = x as FinSequence by FINSEQ_1:def_2;
A7: for i being Element of Seg n holds x . i in the carrier of (F . i)
proof
let i be Element of Seg n; ::_thesis: x . i in the carrier of (F . i)
 ex R being 1-sorted st
( R = F . i & (Carrier F) . i = the carrier of R ) by PRALG_1:def_13;
hence  x . i in the carrier of (F . i) by A6, A5, CARD_3:9; ::_thesis: verum
end;
 for i being Nat st i in dom s holds
s . i in the carrier of G
proof
let i be Nat; ::_thesis: ( i in dom s implies s . i in the carrier of G )
assume  i in dom s ; ::_thesis: s . i in the carrier of G
then reconsider j = i as Element of Seg n by A5, PARTFUN1:def_2;
A8: s . j in the carrier of (F . j) by A7;
 F . j is Subgroup of G by A1;
then  the carrier of (F . j) c= the carrier of G by GROUP_2:def_5;
hence  s . i in the carrier of G by A8; ::_thesis: verum
end;
hence  ( x is FinSequence of G & dom x = Seg n & dom x = dom (Carrier F) & ( for i being set st i in dom (Carrier F) holds
x . i in (Carrier F) . i ) ) by A5, CARD_3:9, FINSEQ_2:12, PARTFUN1:def_2; ::_thesis: verum
end;
defpred S1[ set , set ] means  ex s being FinSequence of G st
( len s = n & ( for k being Element of Seg n holds s . k in F . k ) & s = $1 & $2 = Product s );
A9: for x being Element of (product F) ex y being Element of G st S1[x,y]
proof
let x be Element of (product F); ::_thesis: ex y being Element of G st S1[x,y]
A10: ( x is FinSequence of G & dom x = Seg n & dom x = dom (Carrier F) & ( for i being set st i in dom (Carrier F) holds
x . i in (Carrier F) . i ) ) by A4;
reconsider s = x as FinSequence of G by A4;
A11: dom x = Seg n by A4;
A12: for i being Element of Seg n holds x . i in the carrier of (F . i)
proof
let i be Element of Seg n; ::_thesis: x . i in the carrier of (F . i)
 ex R being 1-sorted st
( R = F . i & (Carrier F) . i = the carrier of R ) by PRALG_1:def_13;
hence  x . i in the carrier of (F . i) by A10; ::_thesis: verum
end;
 n in NAT by ORDINAL1:def_12;
then A13: len s = n by A11, FINSEQ_1:def_3;
A14: now__::_thesis:_for_k_being_Element_of_Seg_n_holds_s_._k_in_F_._k
let k be Element of Seg n; ::_thesis: s . k in F . k
 s . k in the carrier of (F . k) by A12;
hence  s . k in F . k by STRUCT_0:def_5; ::_thesis: verum
end;
take  Product s ; ::_thesis: S1[x, Product s]
thus  S1[x, Product s] by A13, A14; ::_thesis: verum
end;
consider f being Function of (product F),G such that
A15: for x being Element of the carrier of (product F) holds S1[x,f . x] from FUNCT_2:sch_3(A9);
 for a, b being Element of (product F) holds f . (a * b) = (f . a) * (f . b)
proof
let a, b be Element of (product F); ::_thesis: f . (a * b) = (f . a) * (f . b)
A16: ( a is FinSequence of G & dom a = Seg n & dom a = dom (Carrier F) & ( for i being set st i in dom (Carrier F) holds
a . i in (Carrier F) . i ) ) by A4;
reconsider a1 = a as FinSequence of G by A4;
A17: ( b is FinSequence of G & dom b = Seg n & dom b = dom (Carrier F) & ( for i being set st i in dom (Carrier F) holds
b . i in (Carrier F) . i ) ) by A4;
reconsider b1 = b as FinSequence of G by A4;
reconsider ab1 = a * b as FinSequence of G by A4;
A18: now__::_thesis:_for_k_being_Element_of_NAT_st_k_in_dom_ab1_holds_
ab1_._k_=_(a1_/._k)_*_(b1_/._k)
let k be Element of NAT ; ::_thesis: ( k in dom ab1 implies ab1 . k = (a1 /. k) * (b1 /. k) )
assume  k in dom ab1 ; ::_thesis: ab1 . k = (a1 /. k) * (b1 /. k)
then reconsider k0 = k as Element of Seg n by A4;
 ex R being 1-sorted st
( R = F . k0 & (Carrier F) . k0 = the carrier of R ) by PRALG_1:def_13;
then reconsider aa = a . k0 as Element of (F . k0) by A16;
 ex R being 1-sorted st
( R = F . k0 & (Carrier F) . k0 = the carrier of R ) by PRALG_1:def_13;
then reconsider bb = b . k0 as Element of (F . k0) by A17;
A19: aa = a1 /. k0 by A16, PARTFUN1:def_6;
A20: bb = b1 /. k0 by A17, PARTFUN1:def_6;
A21: F . k0 is Subgroup of G by A1;
thus ab1 . k = aa * bb by GROUP_7:1
.= (a1 /. k) * (b1 /. k) by A19, A20, A21, GROUP_2:43 ; ::_thesis: verum
end;
A22: ex sa being FinSequence of G st
( len sa = n & ( for k being Element of Seg n holds sa . k in F . k ) & sa = a & f . a = Product sa ) by A15;
A23: ex sb being FinSequence of G st
( len sb = n & ( for k being Element of Seg n holds sb . k in F . k ) & sb = b & f . b = Product sb ) by A15;
 ex sab being FinSequence of G st
( len sab = n & ( for k being Element of Seg n holds sab . k in F . k ) & sab = a * b & f . (a * b) = Product sab ) by A15;
hence  f . (a * b) = (f . a) * (f . b) by A18, A22, A23, GROUP_4:17; ::_thesis: verum
end;
then reconsider f = f as Homomorphism of (product F),G by GROUP_6:def_6;
take  f ; ::_thesis: ( f is bijective & ( for x being Element of (product F) ex s being FinSequence of G st
( len s = n & ( for k being Element of Seg n holds s . k in F . k ) & s = x & f . x = Product s ) ) )
now__::_thesis:_for_y_being_set_st_y_in_the_carrier_of_G_holds_
y_in_rng_f
let y be set ; ::_thesis: ( y in the carrier of G implies y in rng f )
assume  y in the carrier of G ; ::_thesis: y in rng f
then consider s being FinSequence of G such that
A24: ( len s = n & ( for k being Element of Seg n holds s . k in F . k ) & y = Product s ) by A2;
A25: the carrier of (product F) = product (Carrier F) by GROUP_7:def_2;
A26: dom s = Seg n by A24, FINSEQ_1:def_3;
A27: dom (Carrier F) = Seg n by PARTFUN1:def_2;
A28: for x being set st x in dom (Carrier F) holds
s . x in (Carrier F) . x
proof
let x be set ; ::_thesis: ( x in dom (Carrier F) implies s . x in (Carrier F) . x )
assume  x in dom (Carrier F) ; ::_thesis: s . x in (Carrier F) . x
then reconsider i = x as Element of Seg n ;
A29: s . i in F . i by A24;
 ex R being 1-sorted st
( R = F . i & (Carrier F) . i = the carrier of R ) by PRALG_1:def_13;
hence  s . x in (Carrier F) . x by A29, STRUCT_0:def_5; ::_thesis: verum
end;
reconsider x = s as Element of (product F) by A25, A26, A27, A28, CARD_3:9;
 ex t being FinSequence of G st
( len t = n & ( for k being Element of Seg n holds t . k in F . k ) & t = x & f . x = Product t ) by A15;
hence  y in rng f by A24, FUNCT_2:4; ::_thesis: verum
end;
then A30: the carrier of G c= rng f by TARSKI:def_3;
 rng f = the carrier of G by A30, XBOOLE_0:def_10;
then A31: f is onto by FUNCT_2:def_3;
 for x1, x2 being set st x1 in the carrier of (product F) & x2 in the carrier of (product F) & f . x1 = f . x2 holds
x1 = x2
proof
let x1, x2 be set ; ::_thesis: ( x1 in the carrier of (product F) & x2 in the carrier of (product F) & f . x1 = f . x2 implies x1 = x2 )
assume A32: ( x1 in the carrier of (product F) & x2 in the carrier of (product F) & f . x1 = f . x2 ) ; ::_thesis: x1 = x2
consider s being FinSequence of G such that
A33: ( len s = n & ( for k being Element of Seg n holds s . k in F . k ) & s = x1 & f . x1 = Product s ) by A15, A32;
consider t being FinSequence of G such that
A34: ( len t = n & ( for k being Element of Seg n holds t . k in F . k ) & t = x2 & f . x2 = Product t ) by A15, A32;
thus  x1 = x2 by A3, A33, A32, A34; ::_thesis: verum
end;
then  f is one-to-one by FUNCT_2:19;
hence  ( f is bijective & ( for x being Element of (product F) ex s being FinSequence of G st
( len s = n & ( for k being Element of Seg n holds s . k in F . k ) & s = x & f . x = Product s ) ) ) by A15, A31; ::_thesis: verum
end;

theorem :: GROUP_12:13
for n being non empty Nat
for G, F being Group-like associative commutative multMagma-Family of Seg n st ( for k being Element of Seg n holds F . k = ProjGroup (G,k) ) holds
ex f being Homomorphism of (product F),(product G) st
( f is bijective & ( for x being Element of (product F) ex s being FinSequence of (product G) st
( len s = n & ( for k being Element of Seg n holds s . k in F . k ) & s = x & f . x = Product s ) ) )
proof
let n be non empty Nat; ::_thesis: for G, F being Group-like associative commutative multMagma-Family of Seg n st ( for k being Element of Seg n holds F . k = ProjGroup (G,k) ) holds
ex f being Homomorphism of (product F),(product G) st
( f is bijective & ( for x being Element of (product F) ex s being FinSequence of (product G) st
( len s = n & ( for k being Element of Seg n holds s . k in F . k ) & s = x & f . x = Product s ) ) )
let G, F be Group-like associative commutative multMagma-Family of Seg n; ::_thesis: ( ( for k being Element of Seg n holds F . k = ProjGroup (G,k) ) implies ex f being Homomorphism of (product F),(product G) st
( f is bijective & ( for x being Element of (product F) ex s being FinSequence of (product G) st
( len s = n & ( for k being Element of Seg n holds s . k in F . k ) & s = x & f . x = Product s ) ) ) )
assume A1: for k being Element of Seg n holds F . k = ProjGroup (G,k) ; ::_thesis: ex f being Homomorphism of (product F),(product G) st
( f is bijective & ( for x being Element of (product F) ex s being FinSequence of (product G) st
( len s = n & ( for k being Element of Seg n holds s . k in F . k ) & s = x & f . x = Product s ) ) )
A2: for i being Element of Seg n holds F . i is Subgroup of product G
proof
let i be Element of Seg n; ::_thesis: F . i is Subgroup of product G
 F . i = ProjGroup (G,i) by A1;
hence  F . i is Subgroup of product G ; ::_thesis: verum
end;
A3: for x being Element of (product G) ex s being FinSequence of (product G) st
( len s = n & ( for k being Element of Seg n holds s . k in F . k ) & x = Product s )
proof
let x be Element of (product G); ::_thesis: ex s being FinSequence of (product G) st
( len s = n & ( for k being Element of Seg n holds s . k in F . k ) & x = Product s )
consider s being FinSequence of (product G) such that
A4: ( len s = n & ( for k being Element of Seg n holds s . k in ProjGroup (G,k) ) & x = Product s ) by Th11;
take  s ; ::_thesis: ( len s = n & ( for k being Element of Seg n holds s . k in F . k ) & x = Product s )
 for k being Element of Seg n holds s . k in F . k
proof
let k be Element of Seg n; ::_thesis: s . k in F . k
 s . k in ProjGroup (G,k) by A4;
hence  s . k in F . k by A1; ::_thesis: verum
end;
hence  ( len s = n & ( for k being Element of Seg n holds s . k in F . k ) & x = Product s ) by A4; ::_thesis: verum
end;
 for s, t being FinSequence of (product G) st len s = n & ( for k being Element of Seg n holds s . k in F . k ) & len t = n & ( for k being Element of Seg n holds t . k in F . k ) & Product s = Product t holds
s = t
proof
let s, t be FinSequence of (product G); ::_thesis: ( len s = n & ( for k being Element of Seg n holds s . k in F . k ) & len t = n & ( for k being Element of Seg n holds t . k in F . k ) & Product s = Product t implies s = t )
assume A5: ( len s = n & ( for k being Element of Seg n holds s . k in F . k ) & len t = n & ( for k being Element of Seg n holds t . k in F . k ) & Product s = Product t ) ; ::_thesis: s = t
 for k being Element of Seg n holds
( t . k in ProjGroup (G,k) & s . k in ProjGroup (G,k) )
proof
let k be Element of Seg n; ::_thesis: ( t . k in ProjGroup (G,k) & s . k in ProjGroup (G,k) )
 ( s . k in F . k & t . k in F . k ) by A5;
hence  ( t . k in ProjGroup (G,k) & s . k in ProjGroup (G,k) ) by A1; ::_thesis: verum
end;
hence  s = t by A5, Th10; ::_thesis: verum
end;
hence  ex f being Homomorphism of (product F),(product G) st
( f is bijective & ( for x being Element of (product F) ex s being FinSequence of (product G) st
( len s = n & ( for k being Element of Seg n holds s . k in F . k ) & s = x & f . x = Product s ) ) ) by A2, A3, Th12; ::_thesis: verum
end;