let p, q be sequence of L; p *' q = q *' p
now for i being Element of NAT holds (p *' q) . i = (q *' p) . ilet i be
Element of
NAT ;
(p *' q) . i = (q *' p) . iconsider 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 for k being Nat st k in dom r1 holds
r1 . k = r2 . (((len r2) - k) + 1)let k be
Nat;
( k in dom r1 implies r1 . k = r2 . (((len r2) - k) + 1) )assume A7:
k in dom r1
;
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
;
verum end; then
r1 = Rev r2
by A1, A4, FINSEQ_5:def 3;
hence
(p *' q) . i = (q *' p) . i
by A2, A5, Th2;
verum end;
hence
p *' q = q *' p
; verum