let I be non empty set ; for G being Group
for F being Group-Family of I
for sx, sy being Element of (sum F)
for x, y, xy being finite-support Function of I,G st ( for i being Element of I holds F . i is Subgroup of G ) & ( for i, j being Element of I
for gi, gj being Element of G st i <> j & gi in F . i & gj in F . j holds
gi * gj = gj * gi ) & sx = x & sy = y & sx * sy = xy holds
Product xy = (Product x) * (Product y)
let G be Group; for F being Group-Family of I
for sx, sy being Element of (sum F)
for x, y, xy being finite-support Function of I,G st ( for i being Element of I holds F . i is Subgroup of G ) & ( for i, j being Element of I
for gi, gj being Element of G st i <> j & gi in F . i & gj in F . j holds
gi * gj = gj * gi ) & sx = x & sy = y & sx * sy = xy holds
Product xy = (Product x) * (Product y)
let F be Group-Family of I; for sx, sy being Element of (sum F)
for x, y, xy being finite-support Function of I,G st ( for i being Element of I holds F . i is Subgroup of G ) & ( for i, j being Element of I
for gi, gj being Element of G st i <> j & gi in F . i & gj in F . j holds
gi * gj = gj * gi ) & sx = x & sy = y & sx * sy = xy holds
Product xy = (Product x) * (Product y)
let sx, sy be Element of (sum F); for x, y, xy being finite-support Function of I,G st ( for i being Element of I holds F . i is Subgroup of G ) & ( for i, j being Element of I
for gi, gj being Element of G st i <> j & gi in F . i & gj in F . j holds
gi * gj = gj * gi ) & sx = x & sy = y & sx * sy = xy holds
Product xy = (Product x) * (Product y)
let x, y, xy be finite-support Function of I,G; ( ( for i being Element of I holds F . i is Subgroup of G ) & ( for i, j being Element of I
for gi, gj being Element of G st i <> j & gi in F . i & gj in F . j holds
gi * gj = gj * gi ) & sx = x & sy = y & sx * sy = xy implies Product xy = (Product x) * (Product y) )
assume that
A1:
for i being Element of I holds F . i is Subgroup of G
and
A2:
for i, j being Element of I
for gi, gj being Element of G st i <> j & gi in F . i & gj in F . j holds
gi * gj = gj * gi
and
A3:
( sx = x & sy = y & sx * sy = xy )
; Product xy = (Product x) * (Product y)
reconsider W = (support x) \/ (support y) as finite Subset of I ;
A9:
sx in sum F
;
then
x in product F
by A3, GROUP_2:40;
then reconsider px = x as Element of (product F) ;
A10:
sy in sum F
;
then
y in product F
by A3, GROUP_2:40;
then reconsider py = y as Element of (product F) ;
A11:
sx * sy in sum F
;
then
xy in product F
by A3, GROUP_2:40;
then reconsider pxy = xy as Element of (product F) ;
for i being object st i in support xy holds
i in W
proof
let i be
object ;
( i in support xy implies i in W )
assume A12:
i in support xy
;
i in W
i in W
proof
assume A13:
not
i in W
;
contradiction
reconsider i =
i as
Element of
I by A12;
A14:
( not
i in support x & not
i in support y )
by A13, XBOOLE_0:def 3;
then A15:
x . i = 1_ G
by Def2;
A16:
y . i = 1_ G
by A14, Def2;
A17:
F . i is
Subgroup of
G
by A1;
x . i in F . i
by A3, A9, Th5, GROUP_2:40;
then reconsider fxi =
x . i as
Element of
(F . i) ;
y . i in F . i
by A3, A10, Th5, GROUP_2:40;
then reconsider fyi =
y . i as
Element of
(F . i) ;
xy . i =
(px * py) . i
by A3, GROUP_2:43
.=
fxi * fyi
by GROUP_7:1
.=
(x . i) * (y . i)
by A17, GROUP_2:43
.=
1_ G
by A15, A16, GROUP_1:def 4
;
hence
contradiction
by A12, Def2;
verum
end;
hence
i in W
;
verum
end;
then A22:
support xy c= W
;
A23:
for a being Function of I,G
for i, j being Element of I st a in product F holds
(a . i) * (a . j) = (a . j) * (a . i)
for i, j being Element of I holds (x . i) * (x . j) = (x . j) * (x . i)
by A3, A9, A23, GROUP_2:40;
then A28:
Product x = Product (x | W)
by Th51, XBOOLE_1:7;
for i, j being Element of I holds (y . i) * (y . j) = (y . j) * (y . i)
by A3, A10, A23, GROUP_2:40;
then A34:
Product y = Product (y | W)
by Th51, XBOOLE_1:7;
for i, j being Element of I holds (xy . i) * (xy . j) = (xy . j) * (xy . i)
by A3, A11, A23, GROUP_2:40;
then A40:
Product xy = Product (xy | W)
by A22, Th51;
set cs = canFS W;
reconsider wx = (x | W) * (canFS W) as FinSequence of G by Th50;
reconsider wy = (y | W) * (canFS W) as FinSequence of G by Th50;
reconsider wxy = (xy | W) * (canFS W) as FinSequence of G by Th50;
A41:
rng (canFS W) = W
by FUNCT_2:def 3;
( W = dom (x | W) & W = dom (y | W) & W = dom (xy | W) )
by PARTFUN1:def 2;
then A43:
( dom (canFS W) = dom wx & dom (canFS W) = dom wy & dom (canFS W) = dom wxy )
by A41, RELAT_1:27;
then
( dom (canFS W) = Seg (len wx) & dom (canFS W) = Seg (len wy) & dom (canFS W) = Seg (len wxy) )
by FINSEQ_1:def 3;
then A45:
( len wxy = len wx & len wxy = len wy )
by FINSEQ_1:6;
A50:
Product (x | W) = Product wx
by GROUP_17:def 1;
A51:
Product (y | W) = Product wy
by GROUP_17:def 1;
A55:
for i, j being Nat st i in dom wxy & j in dom wxy & i <> j holds
(wx /. i) * (wy /. j) = (wy /. j) * (wx /. i)
proof
let i,
j be
Nat;
( i in dom wxy & j in dom wxy & i <> j implies (wx /. i) * (wy /. j) = (wy /. j) * (wx /. i) )
assume A56:
(
i in dom wxy &
j in dom wxy &
i <> j )
;
(wx /. i) * (wy /. j) = (wy /. j) * (wx /. i)
then A57:
(
(canFS W) . i in rng (canFS W) &
(canFS W) . j in rng (canFS W) )
by A43, FUNCT_1:3;
then A59:
(
(canFS W) . i in W &
(canFS W) . j in W )
;
A60:
wx /. i =
wx . i
by A43, A56, PARTFUN1:def 6
.=
(x | W) . ((canFS W) . i)
by A43, A56, FUNCT_1:12
.=
x . ((canFS W) . i)
by A57, FUNCT_1:49
;
A61:
wy /. j =
wy . j
by A43, A56, PARTFUN1:def 6
.=
(y | W) . ((canFS W) . j)
by A43, A56, FUNCT_1:12
.=
y . ((canFS W) . j)
by A57, FUNCT_1:49
;
reconsider i0 =
(canFS W) . i as
Element of
I by A59;
reconsider j0 =
(canFS W) . j as
Element of
I by A59;
A64:
x . i0 in F . i0
by A3, A9, Th5, GROUP_2:40;
reconsider gi =
x . i0 as
Element of
G ;
A65:
y . j0 in F . j0
by A3, A10, Th5, GROUP_2:40;
reconsider gj =
y . j0 as
Element of
G ;
thus
(wx /. i) * (wy /. j) = (wy /. j) * (wx /. i)
by A2, A43, A56, A60, A61, A64, A65, FUNCT_1:def 4;
verum
end;
A67:
for i being Nat st i in dom wxy holds
wxy . i = (wx /. i) * (wy /. i)
proof
let i be
Nat;
( i in dom wxy implies wxy . i = (wx /. i) * (wy /. i) )
assume A68:
i in dom wxy
;
wxy . i = (wx /. i) * (wy /. i)
A70:
(canFS W) . i in rng (canFS W)
by A43, A68, FUNCT_1:3;
then A71:
(canFS W) . i in W
;
A72:
wx /. i =
wx . i
by A43, A68, PARTFUN1:def 6
.=
(x | W) . ((canFS W) . i)
by A43, A68, FUNCT_1:12
.=
x . ((canFS W) . i)
by A70, FUNCT_1:49
;
A73:
wy /. i =
wy . i
by A43, A68, PARTFUN1:def 6
.=
(y | W) . ((canFS W) . i)
by A43, A68, FUNCT_1:12
.=
y . ((canFS W) . i)
by A70, FUNCT_1:49
;
A74:
wxy /. i =
wxy . i
by A68, PARTFUN1:def 6
.=
(xy | W) . ((canFS W) . i)
by A68, FUNCT_1:12
.=
xy . ((canFS W) . i)
by A70, FUNCT_1:49
;
reconsider i0 =
(canFS W) . i as
Element of
I by A71;
A75:
F . i0 is
Subgroup of
G
by A1;
x . i0 in F . i0
by A3, A9, Th5, GROUP_2:40;
then reconsider fxi =
x . i0 as
Element of
(F . i0) ;
y . i0 in F . i0
by A3, A10, Th5, GROUP_2:40;
then reconsider fyi =
y . i0 as
Element of
(F . i0) ;
thus wxy . i =
xy . i0
by A68, A74, PARTFUN1:def 6
.=
(px * py) . i0
by A3, GROUP_2:43
.=
fxi * fyi
by GROUP_7:1
.=
(wx /. i) * (wy /. i)
by A72, A73, A75, GROUP_2:43
;
verum
end;
Product wxy = (Product wx) * (Product wy)
by A45, A55, A67, Th47;
hence
Product xy = (Product x) * (Product y)
by A28, A34, A40, A50, A51, GROUP_17:def 1; verum