let I be non empty set ; :: thesis: for G being Group
for a being finite-support Function of I,G
for W being finite Subset of I st support a c= W & ( for i, j being Element of I holds (a . i) * (a . j) = (a . j) * (a . i) ) holds
Product a = Product (a | W)
let G be Group; :: thesis: for a being finite-support Function of I,G
for W being finite Subset of I st support a c= W & ( for i, j being Element of I holds (a . i) * (a . j) = (a . j) * (a . i) ) holds
Product a = Product (a | W)
let a be finite-support Function of I,G; :: thesis: for W being finite Subset of I st support a c= W & ( for i, j being Element of I holds (a . i) * (a . j) = (a . j) * (a . i) ) holds
Product a = Product (a | W)
let W be finite Subset of I; :: thesis: ( support a c= W & ( for i, j being Element of I holds (a . i) * (a . j) = (a . j) * (a . i) ) implies Product a = Product (a | W) )
assume that
A1: support a c= W and
A2: for i, j being Element of I holds (a . i) * (a . j) = (a . j) * (a . i) ; :: thesis: Product a = Product (a | W)
reconsider ra = rng a as non empty Subset of G ;
for x, y being Element of G st x in ra & y in ra holds
x * y = y * x

proof

let x, y be Element of G; :: thesis: ( x in ra & y in ra implies x * y = y * x )
assume A3: ( x in ra & y in ra ) ; :: thesis: x * y = y * x
then consider i being Element of I such that
A4: x = a . i by FUNCT_2:113;
consider j being Element of I such that
A5: y = a . j by A3, FUNCT_2:113;
thus x * y = y * x by A2, A4, A5; :: thesis: verum

end;

then reconsider H = gr ra as non empty commutative Subgroup of G by Th44;
reconsider A = support a as finite Subset of W by A1;
reconsider B = W \ (support a) as finite Subset of W by XBOOLE_1:36;

per cases ( A = {} or A <> {} ) ;

suppose A6: A = {} ; :: thesis: Product a = Product (a | W)

then (a | A) * (canFS A) = {} ;
then A7: Product a = Product (<*> the carrier of G) by GROUP_17:def 1
.= 1_ G by GROUP_4:8 ;
for i being object st i in W holds
(a | W) . i = 1_ G

proof

let i be object ; :: thesis: ( i in W implies (a | W) . i = 1_ G )
assume A8: i in W ; :: thesis: (a | W) . i = 1_ G
then a . i = 1_ G by A6, Def2;
hence (a | W) . i = 1_ G by A8, FUNCT_1:49; :: thesis: verum

end;

hence Product a = Product (a | W) by A7, Th49; :: thesis: verum

end;

suppose A11: A <> {} ; :: thesis: Product a = Product (a | W)

per cases ( B = {} or B <> {} ) ;

suppose B = {} ; :: thesis: Product a = Product (a | W)

then W c= A by XBOOLE_1:37;
then A = W by XBOOLE_0:def 10;
hence Product a = Product (a | W) ; :: thesis: verum

end;

suppose A12: B <> {} ; :: thesis: Product a = Product (a | W)

rng a c= [#] H by GROUP_4:def 4;
then A14: a is Function of I,H by FUNCT_2:6;
then reconsider fa = a | (support a) as A -defined the carrier of H -valued total Function ;
reconsider B0 = B as finite Subset of I ;
reconsider fb = a | B0 as B0 -defined the carrier of H -valued total Function by A14;
A15: A \/ B = W by XBOOLE_1:45;
then reconsider fab = a | W as A \/ B -defined the carrier of H -valued total Function by A14;
A16: A misses B by XBOOLE_1:79;
A17: dom fab = A \/ B by A15, FUNCT_2:def 1
.= (dom fa) \/ B by FUNCT_2:def 1
.= (dom fa) \/ (dom fb) by FUNCT_2:def 1 ;
A18: for x being object st x in dom fab holds
fab . x = (fa +* fb) . x

proof

let x be object ; :: thesis: ( x in dom fab implies fab . x = (fa +* fb) . x )
assume A19: x in dom fab ; :: thesis: fab . x = (fa +* fb) . x

per cases then ( x in dom fa or x in dom fb ) by A17, XBOOLE_0:def 3;

suppose A22: x in dom fa ; :: thesis: fab . x = (fa +* fb) . x

A24: not x in dom fb

proof

assume x in dom fb ; :: thesis: contradiction
then x in A /\ B by A22, XBOOLE_0:def 4;
hence contradiction by XBOOLE_0:def 7, XBOOLE_1:79; :: thesis: verum

end;

thus fab . x = a . x by A19, FUNCT_1:47
.= fa . x by A22, FUNCT_1:47
.= (fa +* fb) . x by A24, FUNCT_4:11 ; :: thesis: verum

end;

suppose A25: x in dom fb ; :: thesis: fab . x = (fa +* fb) . x

thus fab . x = a . x by A19, FUNCT_1:47
.= fb . x by A25, FUNCT_1:47
.= (fa +* fb) . x by A25, FUNCT_4:13 ; :: thesis: verum

end;

end;

end;

A27: dom (fa +* fb) = (dom fa) \/ (dom fb) by FUNCT_4:def 1;
reconsider fca = fa * (canFS A) as FinSequence of H by Th50;
reconsider fcsa = fa * (canFS (support a)) as FinSequence of G by Th50;
reconsider fcab = fab * (canFS (A \/ B)) as FinSequence of H by Th50;
reconsider fcw = (a | W) * (canFS W) as FinSequence of G by Th50;
A31: Product fa = Product fca by GROUP_17:def 1
.= Product fcsa by Th45
.= Product a by GROUP_17:def 1 ;
A35: fcab = fcw by XBOOLE_1:45;
A36: Product fab = Product fcab by GROUP_17:def 1
.= Product fcw by A35, Th45
.= Product (a | W) by GROUP_17:def 1 ;
for i being object st i in B0 holds
fb . i = 1_ H

proof

let i be object ; :: thesis: ( i in B0 implies fb . i = 1_ H )
assume A38: i in B0 ; :: thesis: fb . i = 1_ H
then A39: ( i in W & not i in support a ) by XBOOLE_0:def 5;
i in dom fb by A38, FUNCT_2:def 1;
hence fb . i = a . i by FUNCT_1:47
.= 1_ G by A39, Def2
.= 1_ H by GROUP_2:44 ;
:: thesis: verum

end;

then A41: Product fb = 1_ H by Th49
.= 1_ G by GROUP_2:44 ;
thus Product (a | W) = (Product fa) * (Product fb) by A11, A12, A16, A17, A18, A27, A36, FUNCT_1:2, GROUP_17:8
.= (Product a) * (1_ G) by A31, A41, GROUP_2:43
.= Product a by GROUP_1:def 4 ; :: thesis: verum

end;

end;

end;

end;