let I, J be non empty set ; :: thesis: for G being commutative Group
for x being finite-support Function of I,G
for y being finite-support Function of J,G
for a being Function of I,J st a is bijective & x = y * a holds
Product x = Product y
let G be commutative Group; :: thesis: for x being finite-support Function of I,G
for y being finite-support Function of J,G
for a being Function of I,J st a is bijective & x = y * a holds
Product x = Product y
let x be finite-support Function of I,G; :: thesis: for y being finite-support Function of J,G
for a being Function of I,J st a is bijective & x = y * a holds
Product x = Product y
let y be finite-support Function of J,G; :: thesis: for a being Function of I,J st a is bijective & x = y * a holds
Product x = Product y
let a be Function of I,J; :: thesis: ( a is bijective & x = y * a implies Product x = Product y )
assume that
A1: a is bijective and
A2: x = y * a ; :: thesis: Product x = Product y
A3: dom a = I by FUNCT_2:def 1;
A4: rng a = J by A1, FUNCT_2:def 3;
reconsider Sx = support x as finite set ;
reconsider Sy = support y as finite set ;
reconsider cx = canFS Sx as FinSequence of Sx ;
reconsider cy = canFS Sy as FinSequence of Sy ;
reconsider x1 = x | Sx as Function of Sx,G by FUNCT_2:32;
consider x2 being FinSequence of G such that
A5: Product x1 = Product x2 and
A6: x2 = x1 * cx by GROUP_17:def 1;
reconsider y1 = y | Sy as Function of Sy,G by FUNCT_2:32;
consider y2 being FinSequence of G such that
A7: Product y1 = Product y2 and
A8: y2 = y1 * cy by GROUP_17:def 1;
A9: Sy = a .: Sx by A1, A2, Th15;
A10: card Sx = card Sy

proof

A11: card Sy c= card Sx by A9, CARD_1:66;
reconsider ia = a " as Function of J,I by A1, A4, FUNCT_2:25;
A12: ia is bijective by A1, GROUP_6:63;
y = y * (id J) by FUNCT_2:17
.= y * (a * ia) by A1, A4, FUNCT_2:29
.= x * ia by A2, RELAT_1:36 ;
then Sx = ia .: Sy by A12, Th15;
then card Sx c= card Sy by CARD_1:66;
hence card Sx = card Sy by A11, XBOOLE_0:def 10; :: thesis: verum

end;

reconsider n = card Sx as Nat ;
reconsider a1 = a | Sx as Function of Sx,J by FUNCT_2:32;
A13: dom a1 = Sx by FUNCT_2:def 1;
A14: rng a1 = Sy by A9, RELAT_1:115;
then reconsider a1 = a1 as Function of Sx,Sy by A13, FUNCT_2:1;
A15: len cx = n by FINSEQ_1:93;
then A16: dom cx = Seg n by FINSEQ_1:def 3;
A17: rng cx = Sx by FUNCT_2:def 3;
then reconsider cx = cx as Function of (Seg n),Sx by A16, FUNCT_2:1;
len cy = n by A10, FINSEQ_1:93;
then A18: dom cy = Seg n by FINSEQ_1:def 3;
A19: rng cy = Sy by FUNCT_2:def 3;
then reconsider cy = cy as Function of (Seg n),Sy by A18, FUNCT_2:1;
reconsider icy = cy " as Function of Sy,(Seg n) by A10, FINSEQ_1:95;
reconsider p = (icy * a1) * cx as Function ;
A20: dom a1 = rng cx by A13, FUNCT_2:def 3;
A21: dom icy = rng a1 by A14, A19, FUNCT_1:33;
A22: dom (a1 * cx) = dom cx by A20, RELAT_1:27;
A23: rng (a1 * cx) = rng a1 by A20, RELAT_1:28;
A24: dom p = dom (icy * (a1 * cx)) by RELAT_1:36
.= dom (a1 * cx) by A21, A23, RELAT_1:27
.= dom cx by A20, RELAT_1:27
.= Seg n by A15, FINSEQ_1:def 3 ;
A25: rng p = rng (icy * (a1 * cx)) by RELAT_1:36
.= rng icy by A21, A23, RELAT_1:28
.= Seg n by A18, FUNCT_1:33 ;
reconsider p = p as Function of (Seg n),(Seg n) by A24, A25, FUNCT_2:1;
rng cy = dom y1 by A19, FUNCT_2:def 1;
then A26: dom y2 = Seg n by A8, A18, RELAT_1:27;
a1 is one-to-one by A1, FUNCT_1:52;
then ( p is one-to-one & p is onto ) by A25, FUNCT_2:def 3;
then reconsider p = p as Permutation of (dom y2) by A26;
A27: ( not Sy is empty implies x2 = y2 * p )

proof

assume A28: not Sy is empty ; :: thesis: x2 = y2 * p
A29: dom x1 = Sx by FUNCT_2:def 1;
then A30: dom x2 = Seg n by A6, A16, A17, RELAT_1:27;
for i being object st i in dom x2 holds
x2 . i = (y2 * p) . i

proof

let i be object ; :: thesis: ( i in dom x2 implies x2 . i = (y2 * p) . i )
assume A31: i in dom x2 ; :: thesis: x2 . i = (y2 * p) . i
then A32: i in Seg n by A6, A16, A17, A29, RELAT_1:27;
A33: cx . i in Sx by A16, A17, A30, A31, FUNCT_1:3;
A34: x2 . i = x1 . (cx . i) by A6, A31, FUNCT_1:12
.= x . (cx . i) by A16, A17, A29, A30, A31, FUNCT_1:3, FUNCT_1:47 ;
A35: y1 * (cy * icy) = y1 * (id Sy) by A19, A28, FUNCT_2:29
.= y1 by FUNCT_2:17 ;
A36: y2 * p = (y1 * cy) * (icy * (a1 * cx)) by A8, RELAT_1:36
.= ((y1 * cy) * icy) * (a1 * cx) by RELAT_1:36
.= y1 * (a1 * cx) by A35, RELAT_1:36 ;
A37: (a1 * cx) . i = a1 . (cx . i) by A16, A32, FUNCT_1:13
.= a . (cx . i) by A16, A17, A30, A31, FUNCT_1:3, FUNCT_1:49 ;
(y2 * p) . i = y1 . ((a1 * cx) . i) by A16, A22, A32, A36, FUNCT_1:13
.= y . (a . (cx . i)) by A14, A16, A22, A23, A32, A37, FUNCT_1:3, FUNCT_1:49
.= x2 . i by A2, A3, A33, A34, FUNCT_1:13 ;
hence x2 . i = (y2 * p) . i ; :: thesis: verum

end;

hence x2 = y2 * p by A24, A25, A26, A30, RELAT_1:27; :: thesis: verum

end;

per cases ( Sy is empty or not Sy is empty ) ;

suppose A38: Sy is empty ; :: thesis: Product x = Product y

then Sx is empty by A10;
hence Product x = Product y by A38; :: thesis: verum

end;

suppose not Sy is empty ; :: thesis: Product x = Product y

hence Product x = Product y by A5, A7, A27, GROUP_4:15; :: thesis: verum

end;

end;