let x, y be FinSequence of COMPLEX ; :: thesis: ( 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 ; :: thesis: (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; :: thesis: ( 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 ) ; :: thesis: 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; :: thesis: verum