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 Def6 ;
A6: len (M *') = len M by Def1;

A7: now :: thesis: for i being Nat st 1 <= i & i <= len ((M * F) *') holds
((M * F) *') . i = ((M *') * (F *')) . i

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:1;
len (Line ((M *'),i)) = len (F *') by A1, A3, A4, MATRIX_0:def 7;
then A11: len (mlt ((Line ((M *'),i)),(F *'))) >= 1 by A2, A3, FINSEQ_2:72;
A12: i in Seg (len (M *')) by A5, A6, A8, A9, FINSEQ_1:1;
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, Def6
.= (Sum (mlt (F,((Line ((M *'),i)) *')))) *' by A10, Th39
.= (Sum ((mlt ((Line ((M *'),i)),(F *'))) *')) *' by A1, Th40
.= ((Sum (mlt ((Line ((M *'),i)),(F *')))) *') *' by A11, Th21
.= ((M *') * (F *')) . i by A12, Def6 ;
:: thesis: verum

end;

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