let F be FinSequence of COMPLEX ; :: thesis: for M being Matrix of COMPLEX st len F = width M & len F >= 1 holds
(M * F) *' = (M *' ) * (F *' )
let M be Matrix of COMPLEX ; :: thesis: ( len F = width M & len F >= 1 implies (M * F) *' = (M *' ) * (F *' ) )
assume A1: ( len F = width M & len F >= 1 ) ; :: thesis: (M * F) *' = (M *' ) * (F *' )
A2: len ((M * F) *' ) = len (M * F) by COMPLSP2:def 1
.= len M by Def7 ;
A3: len (M *' ) = len M by Def1;
A4: len (F *' ) = len F by COMPLSP2:def 1;
A5: width (M *' ) = width M by Def1;
A6: len ((M *' ) * (F *' )) = len (M *' ) by Def7
.= len M by Def1 ;

now

let i be Nat; :: thesis: ( 1 <= i & i <= len ((M * F) *' ) implies ((M * F) *' ) . i = ((M *' ) * (F *' )) . i )
assume A7: ( 1 <= i & i <= len ((M * F) *' ) ) ; :: thesis: ((M * F) *' ) . i = ((M *' ) * (F *' )) . i
then A8: i in Seg (len M) by A2, FINSEQ_1:3;
A9: i in Seg (len (M *' )) by A2, A3, A7, FINSEQ_1:3;
len (Line (M *' ),i) = len (F *' ) by A1, A4, A5, MATRIX_1:def 8;
then A10: len (mlt (Line (M *' ),i),(F *' )) >= 1 by A1, A4, FINSEQ_2:86;
( 1 <= i & i <= len (M * F) ) by A7, COMPLSP2:def 1;
hence ((M * F) *' ) . i = ((M * F) . i) *' by COMPLSP2:def 1
.= (Sum (mlt F,(Line M,i))) *' by A8, Def7
.= (Sum (mlt F,((Line (M *' ),i) *' ))) *' by A8, Th43
.= (Sum ((mlt (Line (M *' ),i),(F *' )) *' )) *' by A1, Th44
.= ((Sum (mlt (Line (M *' ),i),(F *' ))) *' ) *' by A10, Th24
.= ((M *' ) * (F *' )) . i by A9, Def7 ;
:: thesis: verum

end;

hence (M * F) *' = (M *' ) * (F *' ) by A2, A6, FINSEQ_1:18; :: thesis: verum