let x, y be FinSequence of COMPLEX ; ( len x = len y implies (mlt (x,(y *'))) *' = mlt (y,(x *')) )
assume A1:
len x = len y
; (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 for i being Nat st 1 <= i & i <= len ((mlt (x,(y *'))) *') holds
((mlt (x,(y *'))) *') . i = (mlt (y,(x *'))) . ilet i be
Nat;
( 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 *'))) *')
;
((mlt (x,(y *'))) *') . i = (mlt (y,(x *'))) . iA9:
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
;
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; verum