let x, y be FinSequence of COMPLEX ; :: thesis: ( len x = len y implies (mlt (x,(y *'))) *' = mlt (y,(x *')) )
assume A1: len x = len y ; :: thesis: (mlt (x,(y *'))) *' = mlt (y,(x *'))
reconsider x19 = x *' as Element of (len (x *')) -tuples_on COMPLEX by FINSEQ_2:92;
reconsider y19 = y as Element of (len y) -tuples_on COMPLEX by FINSEQ_2:92;
reconsider y9 = y *' as Element of (len (y *')) -tuples_on COMPLEX by FINSEQ_2:92;
reconsider x9 = x as Element of (len x) -tuples_on COMPLEX by FINSEQ_2:92;
A2: len (x *') = len x by COMPLSP2:def 1;
A3: len (y *') = len y by COMPLSP2:def 1;
then A4: len (mlt (x,(y *'))) = len x by A1, FINSEQ_2:72;
A5: len (mlt (x,(y *'))) = len (y *') by A1, A3, FINSEQ_2:72;

A6: now :: thesis: for i being Nat st 1 <= i & i <= len ((mlt (x,(y *'))) *') holds
((mlt (x,(y *'))) *') . i = (mlt (y,(x *'))) . i

let i be Nat; :: thesis: ( 1 <= i & i <= len ((mlt (x,(y *'))) *') implies ((mlt (x,(y *'))) *') . i = (mlt (y,(x *'))) . i )
assume that
A7: 1 <= i and
A8: i <= len ((mlt (x,(y *'))) *') ; :: thesis: ((mlt (x,(y *'))) *') . i = (mlt (y,(x *'))) . i
A9: i <= len (mlt (x,(y *'))) by A8, COMPLSP2:def 1;
hence ((mlt (x,(y *'))) *') . i = ((mlt (x,(y *'))) . i) *' by A7, COMPLSP2:def 1
.= ((x9 . i) * (y9 . i)) *' by A1, A3, Th18
.= ((x . i) *') * (((y *') . i) *') by COMPLEX1:35
.= ((x . i) *') * (((y *') *') . i) by A5, A7, A9, COMPLSP2:def 1
.= ((x . i) *') * (y . i)
.= ((x *') . i) * (y . i) by A4, A7, A9, COMPLSP2:def 1
.= (mlt (x19,y19)) . i by A1, A2, Th18
.= (mlt (y,(x *'))) . i ;
:: thesis: verum

end;

len (mlt (x,(y *'))) = len ((mlt (x,(y *'))) *') by COMPLSP2:def 1;
then len ((mlt (x,(y *'))) *') = len (mlt (y,(x *'))) by A1, A2, A4, FINSEQ_2:72;
hence (mlt (x,(y *'))) *' = mlt (y,(x *')) by A6, FINSEQ_1:14; :: thesis: verum