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 that
A1: len F = width M and
A2: len F >= 1 ; :: thesis: (M * F) *' = (M *' ) * (F *' )
A3: len (F *' ) = len F by COMPLSP2:def 1;
A4: width (M *' ) = width M by Def1;
A5: len ((M * F) *' ) = len (M * F) by COMPLSP2:def 1
.= len M by Def7 ;
A6: len (M *' ) = len M by Def1;

A7: now

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

end;

len ((M *' ) * (F *' )) = len (M *' ) by Def7
.= len M by Def1 ;
hence (M * F) *' = (M *' ) * (F *' ) by A5, A7, FINSEQ_1:18; :: thesis: verum