let p, q be Series of n,L; :: thesis: p *' q = q *' p
reconsider pq = p *' q, qp = q *' p as Function of (Bags n), the carrier of L ;

now :: thesis: for b being Element of Bags n holds pq . b = qp . b

let b be Element of Bags n; :: thesis: pq . b = qp . b
defpred S₁[ 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 :: thesis: for e being object st e in ds holds
ex d being object st
( d in ds & S₁[e,d] )

let e be object ; :: thesis: ( e in ds implies ex d being object st
( d in ds & S₁[e,d] ) )
assume A6: e in ds ; :: thesis: ex d being object st
( d in ds & S₁[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; :: thesis: ( d in ds & S₁[e,d] )
thus d in ds by A2, A9, FINSEQ_3:29; :: thesis: S₁[e,d]
thus S₁[e,d] :: thesis: verum

proof

take b1 ; :: thesis: ex b2 being bag of n st
( (decomp b) . e = <*b1,b2*> & (decomp b) . d = <*b2,b1*> )
take b2 ; :: thesis: ( (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; :: thesis: verum

end;

end;

consider f being Function of ds,ds such that
A11: for e being object st e in ds holds
S₁[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 ; :: according to TARSKI:def 3 :: thesis: ( not x in ds or x in rng f )
assume A13: x in ds ; :: thesis: 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; :: thesis: verum

end;

then A20: rng f = ds ;
f is one-to-one

proof

let x1, x2 be object ; :: according to FUNCT_1:def 4 :: thesis: ( 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 ; :: thesis: 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; :: thesis: 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 :: thesis: for i being Nat st i in dom t holds
t . i = s . (f . i)

let i be Nat; :: thesis: ( 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 ; :: thesis: 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; :: thesis: verum

end;

hence pq . b = qp . b by A1, A2, A28, A29, RLVECT_2:6; :: thesis: verum

end;

hence p *' q = q *' p ; :: thesis: verum