:: Normal Subgroup of Product of Groups
:: by Hiroyuki Okazaki , Kenichi Arai and Yasunari Shidama
::
:: Received July 2, 2010
:: Copyright (c) 2010-2026 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies FINSEQ_1, FUNCT_1, RELAT_1, RLVECT_2, CARD_3, TARSKI, BINOP_1,
GROUP_1, XXREAL_0, GROUP_2, CARD_1, NUMBERS, FUNCT_4, GROUP_6, GROUP_7,
FUNCOP_1, ALGSTR_0, GROUP_12, PARTFUN1, FUNCT_2, SUBSET_1, XBOOLE_0,
STRUCT_0, NAT_1, ORDINAL4, PRE_TOPC, ARYTM_1, ARYTM_3, XCMPLX_0;
notations TARSKI, XBOOLE_0, SUBSET_1, XCMPLX_0, RELAT_1, FUNCT_1, RELSET_1,
PARTFUN1, FUNCT_2, FUNCT_4, FUNCOP_1, CARD_3, ORDINAL1, NUMBERS,
FINSEQ_1, XXREAL_0, STRUCT_0, ALGSTR_0, GROUP_1, GROUP_2, GROUP_3,
GROUP_4, GROUP_6, PRALG_1, GROUP_7, FUNCT_7;
constructors BINOP_1, REALSET1, FUNCT_4, GROUP_6, MONOID_0, PRALG_1, GROUP_4,
GROUP_7, FUNCT_7, RELSET_1;
registrations XBOOLE_0, XREAL_0, STRUCT_0, GROUP_2, MONOID_0, ORDINAL1, NAT_1,
FUNCT_2, FUNCOP_1, CARD_1, CARD_3, GROUP_7, XXREAL_0, RELSET_1, FINSEQ_1;
requirements NUMERALS, REAL, BOOLE, SUBSET, ARITHM;
equalities GROUP_2, FINSEQ_1;
expansions FINSEQ_1;
theorems PRALG_1, FUNCT_1, CARD_3, FUNCT_2, TARSKI, GROUP_1, GROUP_2, GROUP_3,
GROUP_4, GROUP_6, FINSEQ_2, XREAL_1, ORDINAL1, FINSEQ_1, FINSEQ_3, NAT_1,
XBOOLE_0, RELAT_1, XXREAL_0, GROUP_7, FUNCT_7, YELLOW17, STRUCT_0,
PARTFUN1;
schemes NAT_1, SUBSET_1, FUNCT_2, FINSEQ_1, XFAMILY;
begin
registration
let I be non empty set, F be Group-like multMagma-Family of I;
let i be Element of I;
cluster F.i -> Group-like for multMagma;
coherence by GROUP_7:def 6;
end;
registration
let I be non empty set, F be associative multMagma-Family of I;
let i be Element of I;
cluster F.i -> associative for multMagma;
coherence by GROUP_7:def 7;
end;
registration
let I be non empty set, F be commutative multMagma-Family of I;
let i be Element of I;
cluster F.i -> commutative for multMagma;
coherence by GROUP_7:def 8;
end;
reserve
I for non empty set,
F for associative Group-like multMagma-Family of I,
i, j for Element of I;
theorem Th1:
for x be Function, g be Element of F.i holds
( dom x = I & x.i = g & for j be Element of I st j <> i holds x.j = 1_F.j )
iff
x = (1_product F)+*(i,g)
proof
let x be Function, g be Element of (F.i);
A1: now assume
A2: x = (1_product F)+* (i,g);
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;
dom x = dom (1_(product F)) by A2,FUNCT_7:30;
hence x.i = g by A2,A4,FUNCT_7:31;
thus for j be Element of I st j <> i holds x.j = 1_F.j
proof
let j be Element of I;
assume j <> i; then
x.j = (1_(product F)).j by A2,FUNCT_7:32;
hence x.j = 1_F.j by GROUP_7:6;
end;
end;
now assume A5:
dom x = I & x.i = g & for j be Element of I st j <>i holds x.j = 1_F.j;
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 let j0 be object;
assume j0 in dom x; then
reconsider j=j0 as Element of I by A5;
per cases;
suppose A8: j <> i; then
x.j = 1_F.j by A5;
hence x.j0 = (1_(product F)).j by GROUP_7:6
.= FG.j0 by A8,FUNCT_7:32;
end;
suppose j = i;
hence x.j0 = FG.j0 by A6,A5,FUNCT_7:31;
end;
end;
hence x = (1_(product F))+* (i,g) by A7,FUNCT_1:2;
end;
hence thesis by A1;
end;
definition
let I be non empty set,
F be associative Group-like multMagma-Family of I,
i be Element of I;
func ProjSet(F,i) -> Subset of product F means :Def1:
for x be set holds x in it iff
ex g be Element of F.i st x = 1_product F +* (i,g);
existence
proof
set CF= the carrier of product F;
defpred P[set] means ex g be Element of F.i
st $1 = (1_(product F))+* (i,g);
consider H be Subset of CF such that
A1: for x be set holds x in H iff x in CF & P[x] from SUBSET_1:sch 1;
take H;
set Gi = F.i;
A2: now let x be set;
assume
A3: P[x];
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 15;
hence x in CF by A3,A4,YELLOW17:2;
end;
let x be set;
x in H iff x in CF & P[x] by A1;
hence thesis by A2;
end;
uniqueness
proof
let F1,F2 be Subset of product F;
defpred P[set] means ex g be Element of F.i st $1 = 1_product F +* (i,g);
assume
A5: for x being set holds x in F1 iff P[x];
assume
A6: for x being set holds x in F2 iff P[x];
thus thesis from XFAMILY:sch 2(A5,A6);
end;
end;
registration
let I be non empty set,
F be associative Group-like multMagma-Family of I,
i be Element of I;
cluster ProjSet(F,i) -> non empty;
coherence
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_Gi)) = dom (1_(product F)) by FUNCT_7:30;
set FG=(1_(product F))+* (i,1_Gi);
reconsider FG as I-defined Function by A2,A1,RELAT_1:def 18;
now let j be Element of I;
per cases;
suppose A3: j <> i;
thus FG.j = (1_(product F)).j by A3,FUNCT_7:32
.= 1_F.j by GROUP_7:6;
end;
suppose j = i;
hence FG.j =1_F.j by A1,FUNCT_7:31;
end;
end;
hence thesis by Def1;
end;
end;
theorem Th2:
for x0 be set holds x0 in ProjSet(F,i) iff
ex x be Function,g be Element of F.i st x = x0 & dom x = I & x.i = g
& for j be Element of I st j <> i holds x.j = 1_F.j
proof
let x0 be set;
defpred P[set] means
ex g be Element of F.i st $1 = (1_(product F))+* (i,g);
A1: now assume x0 in ProjSet(F,i); then
consider g be Element of F.i such that
A2: x0 = (1_(product F))+* (i,g) by Def1;
reconsider x=x0 as Function by A2;
take x,g;
thus x=x0;
thus dom x = I & x.i = g & for j be Element of I st j <> i holds
x.j = 1_F.j by A2,Th1;
end;
now assume
A3: ex x be Function,g be Element of F.i st x=x0 &
dom x = I & x.i = g &
for j be Element of I st j <> i holds x.j = 1_F.j;
thus x0 in ProjSet(F,i)
proof
consider x be Function,g be Element of (F.i) such that
A4: x=x0 & dom x = I & x.i = g &
for j be 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;
end;
end;
hence thesis by A1;
end;
theorem Th3:
for g1,g2 be Element of product F,
z1,z2 be 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 g1,g2 be Element of product F,
z1,z2 be Element of F.i;
assume A1: g1=((1_(product F))+* (i,z1)) &
g2=((1_(product F))+* (i,z2));
set x1=g1, x2 = g2;
A2: x1=g1 & dom x1 = I & x1.i = z1 &
for j be Element of I st j <> i holds x1.j = 1_F.j by Th1,A1;
A3: x2=g2 & dom x2 = I & x2.i = z2 &
for j be Element of I st j <> i holds x2.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 x12 = I by PARTFUN1:def 2;
A5: x12.i = z1*z2 by A2,A3,GROUP_7:1;
for j be Element of I st i <> j holds x12.j = 1_F.j
proof
let j be Element of I;
assume A6: i <> j; then
A7: x1.j = 1_F.j by Th1,A1;
x2.j = 1_F.j by A6,Th1,A1;
hence x12.j = 1_F.j*1_F.j by A7,GROUP_7:1
.= 1_F.j by GROUP_1:def 4;
end;
hence thesis by A4,A5,Th1;
end;
theorem Th4:
for g1 be Element of product F,
z1 be Element of F.i st
g1 = (1_product F)+* (i,z1) holds
g1" = (1_product F)+* (i,z1")
proof
let g1 be Element of product F,
z1 be Element of F.i;
assume A1: g1=1_(product F)+* (i,z1);
set x1=g1;
A2: x1=g1 & dom x1 = I & x1.i = z1 &
for j be Element of I st j <> i holds x1.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 x12 = I by PARTFUN1:def 2;
A4: x12.i = z1" by A2,GROUP_7:8;
A5: for j be Element of I st i <> j holds x12.j = 1_F.j
proof
let j be Element of I;
assume i <> j; then
x1.j = 1_F.j by Th1,A1;
hence x12.j = (1_F.j)" by GROUP_7:8
.= 1_F.j by GROUP_1:8;
end;
thus thesis by A3,A4,A5,Th1;
end;
theorem Th5:
for g1,g2 be Element of product F
st g1 in ProjSet(F,i) & g2 in ProjSet(F,i)
holds g1 * g2 in ProjSet(F,i)
proof
let g1,g2 be Element of product F;
assume A1:
g1 in ProjSet(F,i) & g2 in ProjSet(F,i);
consider z1 be Element of (F.i) such that
A2: g1 = 1_product F +* (i,z1) by Def1,A1;
consider z2 be 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;
end;
theorem Th6:
for g be Element of product F st g in ProjSet(F,i)
holds g" in ProjSet(F,i)
proof
let g be Element of product F;
assume A1: g in ProjSet(F,i);
consider z be 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;
end;
definition
let I be non empty set,
F be associative Group-like multMagma-Family of I,
i be Element of I;
func ProjGroup(F,i) -> strict Subgroup of product F means :Def2:
the carrier of it = ProjSet(F,i);
existence
proof
(for g1,g2 be Element of product F
st g1 in ProjSet(F,i) & g2 in ProjSet(F,i)
holds g1 * g2 in ProjSet(F,i)) &
(for g be Element of product F st g in ProjSet(F,i)
holds g" in ProjSet(F,i)) by Th5,Th6;
hence thesis by GROUP_2:52;
end;
uniqueness by GROUP_2:59;
end;
Lm1:
ex f being Homomorphism of F.i,ProjGroup(F,i)
st f is bijective &
for x be Element of F.i holds f.x = 1_product F +* (i,x)
proof
A1: the carrier of ProjGroup(F,i) = ProjSet(F,i) by Def2;
defpred P[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 P[x,y]
proof
let x be Element of F.i;
1_product F +* (i,x) in ProjSet(F,i) by Def1;
hence thesis by A1;
end;
consider f be Function of F.i,
the carrier of ProjGroup(F,i) such that
A3: for x being Element of the carrier of F.i
holds P[x,f.x] from FUNCT_2:sch 3(A2);
for a,b be Element of F.i holds f.(a*b) = f.a * f.b
proof
let a,b be Element of F.i;
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;
end; then
reconsider f as Homomorphism of F.i,ProjGroup(F,i) by GROUP_6:def 6;
take f;
now let x be object;
assume x in the carrier of (ProjGroup(F,i)); then
consider g be 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;
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 be object 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 object;
assume A10: x1 in the carrier of F.i
& x2 in the carrier of F.i & f.x1 = f.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;
end;
then f is one-to-one by FUNCT_2:19;
hence f is bijective by A9;
thus thesis by A3;
end;
definition let I, F, i;
func 1ProdHom (F,i) -> Homomorphism of F.i, ProjGroup(F,i) means :Def3:
for x be Element of F.i holds it.x = 1_product F +* (i,x);
existence
proof
ex f being Homomorphism of F.i,ProjGroup(F,i) st f is bijective &
for x be Element of F.i holds f.x = 1_product F +* (i,x) by Lm1;
hence thesis;
end;
uniqueness
proof
let F1, F2 be Homomorphism of F.i, ProjGroup(F,i) such that
A1: for x be Element of F.i holds F1.x = 1_product F +* (i,x) and
A2: for x be Element of F.i holds F2.x = 1_product F +* (i,x);
now let x be Element of F.i;
thus F1.x = 1_product F +* (i,x) by A1 .= F2.x by A2;
end;
hence thesis by FUNCT_2:63;
end;
end;
registration let I, F, i;
cluster 1ProdHom (F,i) -> bijective;
coherence
proof
consider f being Homomorphism of F.i,ProjGroup(F,i) such that
A1: f is bijective &
for x be Element of F.i holds f.x = 1_product F +* (i,x) by Lm1;
set F2 = 1ProdHom (F,i);
for x be Element of F.i holds
f.x = F2.x by Def3,A1;
hence thesis by A1,FUNCT_2:63;
end;
end;
registration
let I,F,i;
cluster ProjGroup(F,i) -> normal;
correctness
proof
set H = ProjGroup(F,i);
set G = product F;
A1:for a be Element of G holds (a* H)* a" c= the carrier of H
proof
let a be Element of G;
now let x be object;
assume x in (a*H)*a"; then
consider h be Element of G such that
A2: x = h * a" & h in (a*H) by GROUP_2:28;
consider k be Element of G such that
A3: h = a*k & k in H by A2,GROUP_2:103;
k in the carrier of H by A3,STRUCT_0:def 5;
then k in ProjSet(F,i) by Def2;
then consider m be Function,g be Element of (F.i) such that
A4: m=k & dom m = I & m.i = g &
for j be 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 n = 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 15;
set ak=a*k, ad=a";
reconsider xa=a.i, xk=k.i as Element of Gi by A8,A5,A6,CARD_3:9;
A9: ak.i = xa*xk by GROUP_7:1;
A10: ad.i = xa" by GROUP_7:8;
A11: n.i = (xa*xk)*xa" by A9,A10,GROUP_7:1;
now let j be Element of I;
assume j <> i; 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 15;
reconsider xa=a.j, xk=k.j as Element of Gj by A13,A5,A6,CARD_3:9;
A14: ak.j = xa*xk by GROUP_7:1;
A15: ad.j = xa" by GROUP_7:8;
thus n.j = (xa*xk)*xa" by A14,A15,GROUP_7:1
.= xa*xa" by A12,A4,GROUP_1:def 4
.= 1_Gj by GROUP_1:def 5;
end; then
n in ProjSet(F,i) by A7,A11,Th2;
hence x in the carrier of H by Def2,A2,A3;
end;
hence (a* H)* a" c= the carrier of H by TARSKI:def 3;
end;
A16:for a be Element of G holds a* H c= H* a
proof
let a be Element of G;
A17: (a* H)* a" c= the carrier of H by A1;
A18: a"*a = 1_(product F) by GROUP_1:def 5;
((a* H)* a")*a =(a*(H* a"))*a by GROUP_2:106
.=a*((H* a")*a) by GROUP_2:33
.=a*(H* (a"*a)) by GROUP_2:107
.=a*H by A18,GROUP_2:109;
hence thesis by A17,GROUP_3:5;
end;
A19:for a be Element of G holds H*a c= a*H
proof
let a be Element of G;
A20: (a"* H)* a"" c= the carrier of H by A1;
A21: a*a" = 1_(product F) by GROUP_1:def 5;
a*((a"* H)* a) = a*(a"* (H* a)) by GROUP_2:106
.=(a*a")*(H *a) by GROUP_2:32
.=((a*a")*H) *a by GROUP_2:106
.=H*a by A21,GROUP_2:109;
hence thesis by A20,GROUP_3:5;
end;
for a be Element of G holds a* H = H*a
proof
let a be Element of G;
A22: a* H c= H* a by A16;
H*a c= a*H by A19;
hence thesis by A22,XBOOLE_0:def 10;
end;
hence thesis by GROUP_3:117;
end;
end;
theorem
for x,y be Element of product F st i <> j &
x in ProjGroup(F,i) & y in ProjGroup(F,j) holds x*y = y*x
proof
set G = product F;
let x,y be Element of G;
assume A1: i <> j & x in ProjGroup(F,i) & y in ProjGroup(F,j);
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 be Function,gx be Element of (F.i) such that
A4: xx=x & dom xx = I & xx.i = gx &
for k be Element of I st k <> i holds xx.k = 1_F.k by A3,Th2;
consider yy be Function,gy be Element of (F.j) such that
A5: yy=y & dom yy = I & yy.j = gy &
for k be 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 xy = I by A6,PARTFUN1:def 2;
A8: dom yx = I by A6,PARTFUN1:def 2;
for k be object st k in dom xy holds xy.k = yx.k
proof
let k0 be object;
assume k0 in dom xy;
then reconsider k=k0 as Element of I by A6,PARTFUN1:def 2;
per cases;
suppose A9: k0 <> i & k0 <> j; then
A10: xx.k = 1_F.k by A4;
A11: yy.k = 1_F.k by A9,A5;
xy.k = (1_F.k) * (1_F.k) by A4,A5,A10,A11,GROUP_7:1
.=yx.k by A4,A5,A10,A11,GROUP_7:1;
hence xy.k0 = yx. k0;
end;
suppose A12: k0 = i or k0 = j;
per cases by A12;
suppose A13: k0 = i; then
A14: yy.k = 1_F.k by A1,A5;
reconsider gx as Element of F.k by A13;
xy.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
.=yx.k by A4,A5,A14,A13,GROUP_7:1;
hence xy.k0 = yx. k0;
end;
suppose A15: k0 = j; then
A16: xx.k = 1_F.k by A1,A4;
reconsider gy as Element of F.k by A15;
xy.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
.=yx.k by A4,A5,A16,A15,GROUP_7:1;
hence xy.k0 = yx. k0;
end;
end;
end;
hence thesis by A7,A8,FUNCT_1:2;
end;
reserve n for non zero Nat;
theorem Th8:
for F being associative Group-like multMagma-Family of Seg n,
J be Nat,
GJ be Group
st 1 <= J & J <= n & GJ = F.J holds
for x be Element of product F,
s be FinSequence of product F st len s < J
& (for k be 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 F be associative Group-like multMagma-Family of Seg n,
J be Nat,
GJ be Group;
assume A1: 1<=J & J <= n & GJ=F.J;
defpred P[Nat] means
for x be Element of product F,
s be FinSequence of product F st
len s < J & len s=$1
& (for k be 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: P[0]
proof
let x be Element of product F,
s be FinSequence of product F;
assume A3: len s < J & len s=0
& (for k be Element of Seg n st k in dom s holds s.k
in ProjGroup(F,k)) & x=Product s;
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;
hence x.J = 1_GJ by A1,A4,GROUP_7:6;
end;
A5: for m be Nat st P[m] holds P[m+1]
proof
let m be Nat;
assume A6:P[m];
let x be Element of product F,
s be FinSequence of product F;
assume A7: len s < J & len s=m+1
& (for k be Element of Seg n st k in dom s holds s.k
in ProjGroup(F,k)) & x=Product s;
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 let k be Element of Seg n;
assume A11: k in dom t;
A12: t.k =s.k by A11,FUNCT_1:47;
k in dom s by A11,RELAT_1:57;
hence t.k in ProjGroup(F,k) by A12,A7;
end;
set y=Product t;
A13: m in NAT by ORDINAL1:def 12;
dom s= Seg (m+1) by A7,FINSEQ_1:def 3;
then Seg m c= dom s by A8,FINSEQ_1:5;
then A14:dom t = Seg m by RELAT_1:62;
then A15:len t =m by FINSEQ_1:def 3,A13;
A16: len t = (len s) -1 by A14,A7,FINSEQ_1:def 3,A13;
A17: y.J = 1_GJ by A6,A10,A16,A7,XREAL_1:51;
len s in Seg len s by A9; then
A18: 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;
A19:len t +1 =len s by A14,A7,FINSEQ_1:def 3,A13;
len (t^<* sn *>) = len s by A19,FINSEQ_2:16;
then A20: dom (t^<* sn *>)=Seg len s by FINSEQ_1:def 3
.=dom s by FINSEQ_1:def 3;
A21: s=t^<* sn *>
proof
for k be Nat st k in dom s holds s.k = (t^<* sn *>).k
proof
let k be Nat;
assume k in dom s;
then A22: k in Seg (len t +1) by A19,FINSEQ_1:def 3;
now per cases by A22,FINSEQ_2:7;
case A23:k in Seg len t;
then k in dom t by FINSEQ_1:def 3; then
(t^<* sn *>).k=t.k by FINSEQ_1:def 7
.=s.k by A23,A15,FUNCT_1:49;
hence thesis;
end;
case k= len t +1;
hence thesis by A19,FINSEQ_1:42;
end;
end;
hence thesis;
end;
hence thesis by A20,FINSEQ_1:13;
end;
A24: x = y*sn by A21,A7,GROUP_4:6;
s.len s in ProjGroup(F,ls) by A7,A18; then
s.len s in the carrier of ProjGroup(F,ls) by STRUCT_0:def 5; then
A25:s.len s in ProjSet(F,ls) by Def2;
consider snn be Function,gn be Element of (F.ls) such that
A26: snn=sn & dom snn = Seg n & snn.ls = gn &
for k be Element of Seg n st k <> ls holds snn.k = 1_F.k by A25,Th2;
thus x.J = 1_GJ
proof
reconsider J0=J as Element of Seg n by A1,FINSEQ_1:1;
A27: snn.J0 = 1_F.J0 by A26,A7;
thus x.J =(1_F.J0)*(1_F.J0) by A17,A26,A27,A24,A1,GROUP_7:1
.=1_GJ by A1,GROUP_1:def 4;
end;
end;
for m be Nat holds P[m] from NAT_1:sch 2(A2,A5);
hence thesis;
end;
theorem Th9:
for F be associative Group-like multMagma-Family of Seg n,
x be Element of product F,
s be FinSequence of product F st len s = n
& (for k be Element of Seg n holds s.k in ProjGroup(F,k))
& x = Product s holds
for i be Nat st
1<= i & i<= n holds
ex si be Element of product F st si=s.i & x.i = si.i
proof
let F be associative Group-like multMagma-Family of Seg n;
defpred P[Nat] means for x be Element of product F,
s be FinSequence of product F st
1 <= len s & len s <= $1 & $1 <=n
& (for k be Element of Seg n st k in dom s holds s.k
in ProjGroup(F,k)) & x=Product s holds
for i be Nat st 1<= i & i<=len s holds
ex si be Element of product F st si=s.i & x.i = si.i;
A1: P[ 0 ];
A2: for m be Nat st P[m] holds P[m+1]
proof
let m be Nat;
assume A3: P[m];
let x be Element of product F,
s be FinSequence of product F;
assume A4: 1 <= len s & len s <= m+1 & m+1 <= n
& (for k be Element of Seg n st k in dom s holds s.k
in ProjGroup(F,k)) & x=Product s;
per cases;
suppose m=0; then
A5:len s= 1 by A4,XXREAL_0:1; then
A6: s = <* (s.1) *> by FINSEQ_1:40;
thus for i be Nat st 1<= i & i<=len s holds
ex si be Element of product F st si=s.i & x.i = si.i
proof
let i be Nat;
assume A7: 1<= i & i<=len s;
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;
thus thesis by A7,A6,A4,A5,GROUP_4:9,XXREAL_0:1;
end;
end;
suppose A8: m<>0;
now per cases;
suppose A9: len s <=m;
1 <= len s & len s <= m &m <= n
proof
(m+1)-1 <= n -0 by A4,XREAL_1:13;
hence thesis by A4,A9;
end;
hence for i be Nat st 1<= i & i<=len s holds
ex si be Element of product F
st si=s.i & x.i = si.i by A3,A4;
end;
suppose A10: len s > m;
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;
A14: m in NAT by ORDINAL1:def 12;
dom s= Seg (m+1) by A11,FINSEQ_1:def 3;
then Seg m c= dom s by A13,FINSEQ_1:5;
then dom t = Seg m by RELAT_1:62;
then A15:len t =m by FINSEQ_1:def 3,A14;
A16: 0+1 <= m by A8,NAT_1:13;
A17: (m+1)-1 <= n -0 by A4,XREAL_1:13;
A18: dom s = Seg len s & dom t = Seg len t by FINSEQ_1:def 3;
A19: now let k be Element of Seg n;
assume A20: k in dom t; then
A21: t.k = s.k by FUNCT_1:47;
Seg len t c= Seg len s by A15,A10,FINSEQ_1:5;
hence t.k in ProjGroup(F,k) by A21,A4,A20,A18;
end;
set y=Product t;
A22: len s in Seg len s by A4; then
reconsider sn=s.len s as Element of product F by A18,FINSEQ_2:11;
A23: s=t^<* sn *> by A11,FINSEQ_3:55;
A24: x = y*sn by A23,A4,GROUP_4:6;
s.len s in ProjGroup(F,ls) by A18,A4,A22; then
s.len s in the carrier of ProjGroup(F,ls) by STRUCT_0:def 5; then
A25: s.len s in ProjSet(F,ls) by Def2;
set Gn=F.ls;
consider snn be Function,gn be Element of F.ls such that
A26: snn=sn & dom snn = Seg n & snn.ls = gn &
for k be Element of Seg n st k <> ls holds snn.k = 1_F.k
by A25,Th2;
thus for i be Nat st 1<= i & i<=len s
holds ex si be Element of product F st si=s.i & x.i = si.i
proof
let i be Nat;
assume A27:1<= i & i<=len s;
per cases;
suppose A28: i <> len s; then
A29: i < len s by A27,XXREAL_0:1;
len s = len t + len (<* sn *>) by A23,FINSEQ_1:22
.= len t + 1 by FINSEQ_1:40; then
A30: 1<= i & i<=len t by A27,A29,NAT_1:13;
then consider ti be Element of product F such that
A31: ti=t.i & y.i = ti.i by A3,A17,A19,A15,A16;
A32:t.i =s.i by A30,A23,FINSEQ_1:64;
1<=i & i <= n by A30,A17,A15,XXREAL_0:2; then
reconsider ii=i as Element of Seg n by FINSEQ_1:1;
A33: sn.ii = 1_F.ii by A26,A28;
consider Rii being 1-sorted such that
A34: Rii = F.ii & (Carrier F).ii = the carrier of Rii
by PRALG_1:def 15;
A35:the carrier of product F = product Carrier F
by GROUP_7:def 2;
A36: dom (Carrier F) = Seg n by PARTFUN1:def 2;
reconsider tii=ti.i as Element of F.ii by A34,A35,A36,CARD_3:9;
x.i =tii*(1_F.ii) by A31,A33,A24,GROUP_7:1
.=ti.i by GROUP_1:def 4;
hence thesis by A31,A32;
end;
suppose A37: i = len s;
A38: y.i = 1_Gn by A37,Th8,A19,A10,A15,A12,A27;
x.i =(1_Gn)*gn by A37,A38,A26,A24,GROUP_7:1
.=sn.i by A26,A37,GROUP_1:def 4;
hence thesis by A37;
end;
end;
end;
end;
hence for i be Nat st 1<= i & i<=len s
holds ex si be Element of product F st si=s.i & x.i = si.i;
end;
end;
A39: for m be Nat holds P[m] from NAT_1:sch 2(A1,A2);
thus for x be Element of product F,
s be FinSequence of product F st len s = n
& (for k be Element of Seg n holds s.k in ProjGroup(F,k)) & x=Product s
holds
for i be Nat st 1<= i & i<= n holds
ex si be Element of product F st si=s.i & x.i = si.i
proof
let x be Element of product F, s be FinSequence of product F;
assume A40: len s = n
& (for k be Element of Seg n holds s.k
in ProjGroup(F,k)) & x=Product s;
A41: 1<=len s & len s <= n by A40,NAT_1:14;
for k be Element of Seg n st k in dom s holds s.k in ProjGroup(F,k) by A40;
hence thesis by A40,A41,A39;
end;
end;
theorem Th10:
for F be associative Group-like multMagma-Family of Seg n,
x be Element of product F,
s,t be FinSequence of product F st len s = n
& (for k be Element of Seg n holds s.k in ProjGroup(F,k)) &
x=Product s & len t = n
& (for k be Element of Seg n holds t.k in ProjGroup(F,k))
& x=Product t holds s=t
proof
let F be associative Group-like multMagma-Family of Seg n,
x be Element of product F, s,t be FinSequence of product F;
set I = Seg n;
assume that
A1: len s = n and
A2: (for k be Element of I holds s.k in ProjGroup(F,k)) and
A3: x=Product s and
A4: len t = n and
A5: (for k be Element of I holds t.k in ProjGroup(F,k)) and
A6: x=Product t;
now let i be Nat;
assume A7: 1<=i & i<= n; then
reconsider i0=i as Element of I by FINSEQ_1:1;
consider si be Element of product F such that
A8: si=s.i & x.i = si.i by A1,A2,A3,A7,Th9;
consider ti be 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 be Function,gn be Element of (F.i0) such that
A11:sn=si & dom sn = I & sn.i0 = gn &
for k be Element of I 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 be Function,fn be Element of (F.i0) such that
A13: tn=ti & dom tn = I & tn.i0 = fn &
for k be Element of I st k <> i0 holds tn.k = 1_F.k by A9,A12,Th2;
now let x be object;
assume x in dom sn; then
reconsider j=x as Element of I by A11;
per cases;
suppose j=i;
hence sn.x=tn.x by A8,A9,A11,A13;
end;
suppose A14: j<>i; then
sn.j = 1_F.j by A11;
hence sn.x=tn.x by A14,A13;
end;
end;
hence s.i = t.i by A8,A9,A11,A13,FUNCT_1:2;
end;
hence thesis by A1,A4;
end;
theorem Th11:
for F be associative Group-like multMagma-Family of Seg n,
x be Element of product F
ex s be FinSequence of product F st len s = n &
(for k be Element of Seg n holds s.k in ProjGroup(F,k)) & x=Product s
proof
let F be associative Group-like multMagma-Family of Seg n,
x be Element of product F;
set I = Seg n;
defpred P[Nat,set] means
ex k be Element of I,g be Element of F.k st k=$1 &
x.k=g & $2=(1_product F)+* (k,g);
A1: for k be Nat st k in Seg n
ex z being Element of product F st P[k,z]
proof
let k be Nat;
assume k in Seg n; then
reconsider k0=k as Element of I;
A2: the carrier of product F = product Carrier F by GROUP_7:def 2;
A3: dom Carrier F = I 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 15;
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;
thus P[k,z];
end;
consider s be FinSequence of product F such that
A5: dom s= Seg n & for k be Nat st k in Seg n holds P[k,s.k]
from FINSEQ_1:sch 5(A1);
take s;
n in NAT by ORDINAL1:def 12;
hence A6: len s = n by A5,FINSEQ_1:def 3;
thus A7: for k be Element of I holds s.k in ProjGroup(F,k)
proof
let k be Element of Seg n;
ex k0 be Element of I,g be 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 thesis by A8,STRUCT_0:def 5;
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 y = Seg n by A9,PARTFUN1:def 2;
A12: dom (1_product F)= I by A9,PARTFUN1:def 2;
now let t be object;
assume t in dom x; 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 be Element of product F st
si=s.i & y.i = si.i by Th9,A6,A7;
ex i1 be Element of I,g be Element of F.i1 st i1=i &
x.i1=g & s.i=(1_product F)+* (i1,g) by A13,A5;
hence x.t=y.t by A12,A14,FUNCT_7:31;
end;
hence thesis by A10,A11,FUNCT_1:2;
end;
theorem Th12:
for G being commutative Group,
F being associative Group-like multMagma-Family of Seg n
st (for i be Element of Seg n holds F.i is Subgroup of G)
& (for x be Element of G
ex s be FinSequence of G st len s = n
& (for k be Element of Seg n holds s.k in F.k) & x=Product s )
& ( for s,t be FinSequence of G st
len s = n & (for k be Element of Seg n holds s.k in F.k) & len t = n
& (for k be 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 be Element of product F
ex s be FinSequence of G st len s= n &
(for k be Element of Seg n holds s.k in F.k) & s=x & f.x = Product s
proof
let G be commutative Group,
F be associative Group-like multMagma-Family of Seg n;
set I = Seg n;
assume that
A1: for i be Element of I holds F.i is Subgroup of G and
A2: for x be Element of G ex s be FinSequence of G st
len s = n
& (for k be Element of I holds s.k in F.k) & x=Product s and
A3: for s,t be FinSequence of G st
len s = n & (for k be Element of I holds s.k in F.k)
& len t = n & (for k be Element of I holds t.k in F.k)
& Product s=Product t holds s=t;
A4: for x being Element of product F
holds x is FinSequence of G & dom x = I &
dom x = dom (Carrier F) &
for i be set st i in dom (Carrier F) holds x.i in (Carrier F).i
proof
let x be Element of product F;
A5: the carrier of product F = product Carrier F by GROUP_7:def 2;
A6: dom (Carrier F) = I 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 be Element of I holds x.i in the carrier of (F.i)
proof
let i be Element of I;
ex R being 1-sorted st R = F.i &
(Carrier F).i = the carrier of R by PRALG_1:def 15;
hence x.i in the carrier of (F.i) by A6,A5,CARD_3:9;
end;
for i be Nat st i in dom s holds s.i in the carrier of G
proof
let i be Nat;
assume i in dom s; then
reconsider j=i as Element of I 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;
end;
hence thesis by A5,CARD_3:9,FINSEQ_2:12,PARTFUN1:def 2;
end;
defpred P[set,set] means ex s be FinSequence of G st len s= n &
(for k be Element of I 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 P[x,y]
proof
let x be Element of product F;
A10: x is FinSequence of G & dom x = I & dom x = dom (Carrier F) &
for i be 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 be Element of I holds x.i in the carrier of (F.i)
proof
let i be Element of I;
ex R being 1-sorted st R = F.i &
(Carrier F).i = the carrier of R by PRALG_1:def 15;
hence x.i in the carrier of (F.i) by A10;
end;
n in NAT by ORDINAL1:def 12; then
A13:len s=n by A11,FINSEQ_1:def 3;
A14:now let k be Element of I;
s.k in the carrier of (F.k) by A12;
hence s.k in F.k by STRUCT_0:def 5;
end;
take Product s;
thus P[x,Product s] by A13,A14;
end;
consider f be Function of product F, G such that
A15: for x being Element of (the carrier of product F)
holds P[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;
A16:a is FinSequence of G & dom a = I &
dom a = dom (Carrier F) &
for i be 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 = I &
dom b = dom (Carrier F) &
for i be 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 let k be Nat;
assume k in dom(ab1);
then reconsider k0= k as Element of I by A4;
ex R being 1-sorted st R = F.k0 &
(Carrier F).k0 = the carrier of R by PRALG_1:def 15; 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 15; 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;
end;
A22: ex sa be FinSequence of G st len sa= n &
(for k be Element of I holds sa.k in F.k) & sa=a
& f.a = Product sa by A15;
A23:ex sb be FinSequence of G st len sb= n &
(for k be Element of I holds sb.k in F.k) & sb=b
& f.b = Product sb by A15;
ex sab be FinSequence of G st len sab= n &
(for k be Element of I holds sab.k in F.k) & sab=a*b
& f.(a*b) = Product sab by A15;
hence thesis by A18,A22,A23,GROUP_4:17;
end; then
reconsider f as Homomorphism of product F,G by GROUP_6:def 6;
take f;
now let y be object;
assume y in the carrier of G; then
consider s be FinSequence of G such that
A24: len s = n
& (for k be Element of I 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 = I by A24,FINSEQ_1:def 3;
A27: dom Carrier F = I by PARTFUN1:def 2;
A28: for x be object st x in dom Carrier F holds s.x in (Carrier F).x
proof
let x be object;
assume x in dom Carrier F;
then reconsider i=x as Element of I;
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 15;
hence s.x in (Carrier F).x by A29,STRUCT_0:def 5;
end;
reconsider x=s as Element of product F by A25,A26,A27,A28,CARD_3:9;
ex t be FinSequence of G st len t= n &
(for k be Element of I holds t.k in F.k) & t=x
& f.x = Product t by A15;
hence y in rng f by A24,FUNCT_2:4;
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 be object 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 object;
assume A32: x1 in the carrier of product F
& x2 in the carrier of product F & f.x1=f.x2;
consider s be FinSequence of G such that
A33: len s= n & (for k be Element of I holds s.k in F.k) & s=x1
& f.x1 = Product s by A15,A32;
consider t be FinSequence of G such that A34: len t= n &
(for k be Element of I holds t.k in F.k) & t=x2
& f.x2 = Product t by A15,A32;
thus x1=x2 by A3,A33,A32,A34;
end;
then f is one-to-one by FUNCT_2:19;
hence thesis by A15,A31;
end;
theorem
for G,F being associative commutative Group-like multMagma-Family of Seg n
st
for k be 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 be Element of product F
ex s be FinSequence of product G st len s= n &
(for k be Element of Seg n holds s.k in F.k) & s=x & f.x = Product s
proof
let G,F be associative commutative Group-like
multMagma-Family of Seg n;
assume A1: for k be Element of Seg n
holds F.k = ProjGroup(G,k);
A2: for i be Element of Seg n holds F.i is Subgroup of product G
proof
let i be Element of Seg n;
F.i = ProjGroup(G,i) by A1;
hence thesis;
end;
A3: for x be Element of product G
ex s be FinSequence of product G st len s = n
& (for k be Element of Seg n holds s.k in F.k) & x=Product s
proof
let x be Element of product G;
consider s be FinSequence of product G such that
A4: len s = n
& (for k be Element of Seg n holds s.k in ProjGroup(G,k)) &
x=Product s by Th11;
take s;
for k be Element of Seg n holds s.k in F.k
proof
let k be Element of Seg n;
s.k in ProjGroup(G,k) by A4;
hence thesis by A1;
end;
hence thesis by A4;
end;
for s,t be FinSequence of product G st
len s = n & (for k be Element of Seg n holds s.k in F.k) & len t = n
& (for k be 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;
assume A5:
len s = n & (for k be Element of Seg n holds s.k in F.k) &
len t = n & (for k be Element of Seg n holds t.k in F.k) &
Product s=Product t;
for k be 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;
s.k in F.k & t.k in F.k by A5;
hence thesis by A1;
end;
hence thesis by A5,Th10;
end;
hence thesis by A2,A3,Th12;
end;