let F be FinSequence of COMPLEX ; 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; ( len F = width M & len F >= 1 implies (M * F) *' = (M *') * (F *') )
assume that
A1:
len F = width M
and
A2:
len F >= 1
; (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 for i being Nat st 1 <= i & i <= len ((M * F) *') holds
((M * F) *') . i = ((M *') * (F *')) . ilet i be
Nat;
( 1 <= i & i <= len ((M * F) *') implies ((M * F) *') . i = ((M *') * (F *')) . i )assume that A8:
1
<= i
and A9:
i <= len ((M * F) *')
;
((M * F) *') . i = ((M *') * (F *')) . iA10:
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
;
verum end;
len ((M *') * (F *')) =
len (M *')
by Def6
.=
len M
by Def1
;
hence
(M * F) *' = (M *') * (F *')
by A5, A7, FINSEQ_1:14; verum