let p, q be Series of n,L; p *' q = q *' p
reconsider pq = p *' q, qp = q *' p as Function of (Bags n), the carrier of L ;
now for b being Element of Bags n holds pq . b = qp . blet b be
Element of
Bags n;
pq . b = qp . bdefpred S1[
object ,
object ]
means ex
b1,
b2 being
bag of
n st
(
(decomp b) . $1
= <*b1,b2*> &
(decomp b) . $2
= <*b2,b1*> );
consider s being
FinSequence of the
carrier of
L such that A1:
pq . b = Sum s
and A2:
len s = len (decomp b)
and A3:
for
k being
Element of
NAT st
k in dom s holds
ex
b1,
b2 being
bag of
n st
(
(decomp b) /. k = <*b1,b2*> &
s /. k = (p . b1) * (q . b2) )
by Def10;
A4:
dom s = dom (decomp b)
by A2, FINSEQ_3:29;
then reconsider ds =
dom s as non
empty set ;
A5:
now for e being object st e in ds holds
ex d being object st
( d in ds & S1[e,d] )let e be
object ;
( e in ds implies ex d being object st
( d in ds & S1[e,d] ) )assume A6:
e in ds
;
ex d being object st
( d in ds & S1[e,d] )then consider b1,
b2 being
bag of
n such that A7:
(decomp b) /. e = <*b1,b2*>
and A8:
b = b1 + b2
by A4, PRE_POLY:68;
consider d being
Element of
NAT such that A9:
d in dom (decomp b)
and A10:
(decomp b) /. d = <*b2,b1*>
by A8, PRE_POLY:69;
reconsider d =
d as
object ;
take d =
d;
( d in ds & S1[e,d] )thus
d in ds
by A2, A9, FINSEQ_3:29;
S1[e,d]thus
S1[
e,
d]
verumproof
take
b1
;
ex b2 being bag of n st
( (decomp b) . e = <*b1,b2*> & (decomp b) . d = <*b2,b1*> )
take
b2
;
( (decomp b) . e = <*b1,b2*> & (decomp b) . d = <*b2,b1*> )
thus
(
(decomp b) . e = <*b1,b2*> &
(decomp b) . d = <*b2,b1*> )
by A4, A6, A7, A9, A10, PARTFUN1:def 6;
verum
end; end; consider f being
Function of
ds,
ds such that A11:
for
e being
object st
e in ds holds
S1[
e,
f . e]
from FUNCT_2:sch 1(A5);
A12:
dom f = ds
by FUNCT_2:def 1;
ds c= rng f
proof
let x be
object ;
TARSKI:def 3 ( not x in ds or x in rng f )
assume A13:
x in ds
;
x in rng f
then consider b1,
b2 being
bag of
n such that A14:
(decomp b) . x = <*b1,b2*>
and A15:
(decomp b) . (f . x) = <*b2,b1*>
by A11;
A16:
f . x in rng f
by A12, A13, FUNCT_1:def 3;
then A17:
f . (f . x) in rng f
by A12, FUNCT_1:def 3;
consider b3,
b4 being
bag of
n such that A18:
(decomp b) . (f . x) = <*b3,b4*>
and A19:
(decomp b) . (f . (f . x)) = <*b4,b3*>
by A11, A16;
(
b3 = b2 &
b4 = b1 )
by A15, A18, FINSEQ_1:77;
hence
x in rng f
by A4, A13, A17, A14, A19, FUNCT_1:def 4;
verum
end; then A20:
rng f = ds
;
f is
one-to-one
proof
let x1,
x2 be
object ;
FUNCT_1:def 4 ( not x1 in dom f or not x2 in dom f or not f . x1 = f . x2 or x1 = x2 )
assume that A21:
x1 in dom f
and A22:
x2 in dom f
and A23:
f . x1 = f . x2
;
x1 = x2
consider b3,
b4 being
bag of
n such that A24:
(decomp b) . x2 = <*b3,b4*>
and A25:
(decomp b) . (f . x2) = <*b4,b3*>
by A11, A22;
consider b1,
b2 being
bag of
n such that A26:
(decomp b) . x1 = <*b1,b2*>
and A27:
(decomp b) . (f . x1) = <*b2,b1*>
by A11, A21;
(
b2 = b4 &
b1 = b3 )
by A23, A27, A25, FINSEQ_1:77;
hence
x1 = x2
by A4, A21, A22, A26, A24, FUNCT_1:def 4;
verum
end; then reconsider f =
f as
Permutation of
(dom s) by A20, FUNCT_2:57;
consider t being
FinSequence of the
carrier of
L such that A28:
qp . b = Sum t
and A29:
len t = len (decomp b)
and A30:
for
k being
Element of
NAT st
k in dom t holds
ex
b1,
b2 being
bag of
n st
(
(decomp b) /. k = <*b1,b2*> &
t /. k = (q . b1) * (p . b2) )
by Def10;
A31:
dom t = dom (decomp b)
by A29, FINSEQ_3:29;
now for i being Nat st i in dom t holds
t . i = s . (f . i)let i be
Nat;
( i in dom t implies t . i = s . (f . i) )reconsider fi =
f . i as
Element of
NAT ;
A32:
dom s = dom (decomp b)
by A2, FINSEQ_3:29;
assume A33:
i in dom t
;
t . i = s . (f . i)then consider b1,
b2 being
bag of
n such that A34:
(decomp b) /. i = <*b1,b2*>
and A35:
t /. i = (q . b1) * (p . b2)
by A30;
A36:
t /. i = t . i
by A33, PARTFUN1:def 6;
consider b5,
b6 being
bag of
n such that A37:
(decomp b) . i = <*b5,b6*>
and A38:
(decomp b) . (f . i) = <*b6,b5*>
by A4, A31, A11, A33;
dom s = dom t
by A2, A29, FINSEQ_3:29;
then
(decomp b) /. i = (decomp b) . i
by A33, A32, PARTFUN1:def 6;
then A39:
(
b1 = b5 &
b2 = b6 )
by A34, A37, FINSEQ_1:77;
A40:
f . i in rng f
by A4, A31, A12, A33, FUNCT_1:def 3;
then A41:
s /. fi = s . fi
by PARTFUN1:def 6;
consider b3,
b4 being
bag of
n such that A42:
(decomp b) /. fi = <*b3,b4*>
and A43:
s /. fi = (p . b3) * (q . b4)
by A3, A40;
A44:
(decomp b) /. fi = (decomp b) . fi
by A40, A32, PARTFUN1:def 6;
then
b3 = b6
by A42, A38, FINSEQ_1:77;
hence
t . i = s . (f . i)
by A35, A42, A43, A38, A36, A41, A44, A39, FINSEQ_1:77;
verum end; hence
pq . b = qp . b
by A1, A2, A28, A29, RLVECT_2:6;
verum end;
hence
p *' q = q *' p
; verum