let I, J be non empty set ; 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; 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; 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; 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; ( a is bijective & x = y * a implies Product x = Product y )
assume that
A1:
a is bijective
and
A2:
x = y * a
; 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;
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
;
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 ;
( i in dom x2 implies x2 . i = (y2 * p) . i )
assume A31:
i in dom x2
;
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
;
verum
end;
hence
x2 = y2 * p
by A24, A25, A26, A30, RELAT_1:27;
verum
end;