let x, y be FinSequence of COMPLEX ; ( len x = len y implies (mlt (x,y)) *' = mlt ((x *'),(y *')) )
A1:
len ((mlt (x,y)) *') = len (mlt (x,y))
by COMPLSP2:def 1;
A2:
len (x *') = len x
by COMPLSP2:def 1;
assume A3:
len x = len y
; (mlt (x,y)) *' = mlt ((x *'),(y *'))
A4:
for i being Nat st 1 <= i & i <= len ((mlt (x,y)) *') holds
((mlt (x,y)) *') . i = (mlt ((x *'),(y *'))) . i
proof
let i be
Nat;
( 1 <= i & i <= len ((mlt (x,y)) *') implies ((mlt (x,y)) *') . i = (mlt ((x *'),(y *'))) . i )
((mlt (x,y)) *') . i =
((mlt (y,((x *') *'))) *') . i
.=
(mlt ((x *'),(y *'))) . i
by A3, A2, Th22
;
hence
( 1
<= i &
i <= len ((mlt (x,y)) *') implies
((mlt (x,y)) *') . i = (mlt ((x *'),(y *'))) . i )
;
verum
end;
len (y *') = len y
by COMPLSP2:def 1;
then
len (mlt ((x *'),(y *'))) = len (x *')
by A3, A2, FINSEQ_2:72;
then
len ((mlt (x,y)) *') = len (mlt ((x *'),(y *')))
by A3, A1, A2, FINSEQ_2:72;
hence
(mlt (x,y)) *' = mlt ((x *'),(y *'))
by A4, FINSEQ_1:14; verum