let x, y be FinSequence of COMPLEX ; :: thesis: ( len x = len y implies (mlt x,y) *' = mlt (x *' ),(y *' ) )
assume A1: len x = len y ; :: thesis: (mlt x,y) *' = mlt (x *' ),(y *' )
A2: len ((mlt x,y) *' ) = len (mlt x,y) by COMPLSP2:def 1;
A3: len (y *' ) = len y by COMPLSP2:def 1;
A4: len (x *' ) = len x by COMPLSP2:def 1;
then len (mlt (x *' ),(y *' )) = len (x *' ) by A1, A3, FINSEQ_2:86;
then A5: len ((mlt x,y) *' ) = len (mlt (x *' ),(y *' )) by A1, A2, A4, FINSEQ_2:86;
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 by COMPLSP2:22
.= (mlt (x *' ),(y *' )) . i by A1, A4, Th25 ;
hence ( 1 <= i & i <= len ((mlt x,y) *' ) implies ((mlt x,y) *' ) . i = (mlt (x *' ),(y *' )) . i ) ; :: thesis: verum

end;

hence (mlt x,y) *' = mlt (x *' ),(y *' ) by A5, FINSEQ_1:18; :: thesis: verum