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:110;
reconsider y19 = y as Element of (len y) -tuples_on COMPLEX by FINSEQ_2:110;
reconsider y9 = y *' as Element of (len (y *' )) -tuples_on COMPLEX by FINSEQ_2:110;
reconsider x9 = x as Element of (len x) -tuples_on COMPLEX by FINSEQ_2:110;
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:86;
A5: len (mlt x,(y *' )) = len (y *' ) by A1, A3, FINSEQ_2:86;

A6: now

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, Th20
.= ((x . i) *' ) * (((y *' ) . i) *' ) by COMPLEX1:121
.= ((x . i) *' ) * (((y *' ) *' ) . i) by A5, A7, A9, COMPLSP2:def 1
.= ((x . i) *' ) * (y . i) by COMPLSP2:22
.= ((x *' ) . i) * (y . i) by A4, A7, A9, COMPLSP2:def 1
.= (mlt x19,y19) . i by A1, A2, Th20
.= (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:86;
hence (mlt x,(y *' )) *' = mlt y,(x *' ) by A6, FINSEQ_1:18; :: thesis: verum