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

hence
p *' q = q *' p
; :: thesis: verumlet 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;

hence (p *' q) . i = (q *' p) . i by A2, A5, Th2; :: thesis: verum

end;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)

then
r1 = Rev r2
by A1, A4, FINSEQ_5:def 3;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;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

hence (p *' q) . i = (q *' p) . i by A2, A5, Th2; :: thesis: verum