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 ;
then A10: (i + 1) - k >= 0 by XREAL_1:48;
then reconsider k1 = ((len r2) - k) + 1 as Element of NAT by ;
A11: (i + 1) -' k = (((i + 1) - k) + 1) - 1 by
.= k1 -' 1 by ;
1 - k <= 0 by ;
then i + (1 - k) <= i + 0 by XREAL_1:6;
then A12: k1 <= i + 1 by ;
then (i + 1) - k1 >= 0 by XREAL_1:48;
then A13: (i + 1) -' k1 = (i + 1) - ((i + 1) - (k - 1)) by
.= k -' 1 by ;
((i + 1) - k) + 1 >= 0 + 1 by ;
then A14: k1 in dom r2 by ;
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 ;
hence (p *' q) . i = (q *' p) . i by A2, A5, Th2; :: thesis: verum
end;
hence p *' q = q *' p ; :: thesis: verum