let p, q be sequence of L; :: thesis: p *' q = q *' p

now :: thesis: for i being Element of NAT holds (p *' q) . i = (q *' p) . i

let i be Element of NAT ; :: thesis: (p *' q) . i = (q *' p) . i
consider r1 being FinSequence of the carrier of L such that
A1: len r1 = i + 1 and
A2: (p *' q) . i = Sum r1 and
A3: for k being Element of NAT st k in dom r1 holds
r1 . k = (p . (k -' 1)) * (q . ((i + 1) -' k)) by Def9;
consider r2 being FinSequence of the carrier of L such that
A4: len r2 = i + 1 and
A5: (q *' p) . i = Sum r2 and
A6: for k being Element of NAT st k in dom r2 holds
r2 . k = (q . (k -' 1)) * (p . ((i + 1) -' k)) by Def9;

now :: thesis: for k being Nat st k in dom r1 holds
r1 . k = r2 . (((len r2) - k) + 1)

let k be Nat; :: thesis: ( k in dom r1 implies r1 . k = r2 . (((len r2) - k) + 1) )
assume A7: k in dom r1 ; :: thesis: r1 . k = r2 . (((len r2) - k) + 1)
then A8: 1 <= k by FINSEQ_3:25;
then A9: k - 1 >= 0 by XREAL_1:48;
k <= i + 1 by A1, A7, FINSEQ_3:25;
then A10: (i + 1) - k >= 0 by XREAL_1:48;
then reconsider k1 = ((len r2) - k) + 1 as Element of NAT by A4, INT_1:3;
A11: (i + 1) -' k = (((i + 1) - k) + 1) - 1 by A10, XREAL_0:def 2
.= k1 -' 1 by A4, A10, XREAL_0:def 2 ;
1 - k <= 0 by A8, XREAL_1:47;
then i + (1 - k) <= i + 0 by XREAL_1:6;
then A12: k1 <= i + 1 by A4, XREAL_1:6;
then (i + 1) - k1 >= 0 by XREAL_1:48;
then A13: (i + 1) -' k1 = (i + 1) - ((i + 1) - (k - 1)) by A4, XREAL_0:def 2
.= k -' 1 by A9, XREAL_0:def 2 ;
((i + 1) - k) + 1 >= 0 + 1 by A10, XREAL_1:6;
then A14: k1 in dom r2 by A4, A12, FINSEQ_3:25;
thus r1 . k = (p . (k -' 1)) * (q . ((i + 1) -' k)) by A3, A7
.= r2 . (((len r2) - k) + 1) by A6, A14, A13, A11 ; :: thesis: verum

end;

then r1 = Rev r2 by A1, A4, FINSEQ_5:def 3;
hence (p *' q) . i = (q *' p) . i by A2, A5, Th2; :: thesis: verum

end;

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