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 by COMPLSP2:22
.= (mlt (x *' ),(y *' )) . i by A3, A2, Th25 ;
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:86;
then len ((mlt x,y) *' ) = len (mlt (x *' ),(y *' )) by A3, A1, A2, FINSEQ_2:86;
hence (mlt x,y) *' = mlt (x *' ),(y *' ) by A4, FINSEQ_1:18; :: thesis: verum