let n, m, i be Nat; :: thesis: for f being n -element real-valued FinSequence
for M being Matrix of n,m,F_Real st 1 <= i & i <= m & n <> 0 holds
((Mx2Tran M) . f) . i = (@ f) "*" (Col (M,i))
let f be n -element real-valued FinSequence; :: thesis: for M being Matrix of n,m,F_Real st 1 <= i & i <= m & n <> 0 holds
((Mx2Tran M) . f) . i = (@ f) "*" (Col (M,i))
let M be Matrix of n,m,F_Real; :: thesis: ( 1 <= i & i <= m & n <> 0 implies ((Mx2Tran M) . f) . i = (@ f) "*" (Col (M,i)) )
assume that
A1: ( 1 <= i & i <= m ) and
A2: n <> 0 ; :: thesis: ((Mx2Tran M) . f) . i = (@ f) "*" (Col (M,i))
A3: len M = n by A2, MATRIX13:1;
set Lf = LineVec2Mx (@ f);
set LfM = (LineVec2Mx (@ f)) * M;
len f = n by CARD_1:def 7;
then A4: width (LineVec2Mx (@ f)) = n by MATRIX13:1;
width M = m by A2, MATRIX13:1;
then A5: width ((LineVec2Mx (@ f)) * M) = m by A4, A3, MATRIX_3:def 4;
len (LineVec2Mx (@ f)) = 1 by MATRIX13:1;
then len ((LineVec2Mx (@ f)) * M) = 1 by A4, A3, MATRIX_3:def 4;
then A6: [1,i] in Indices ((LineVec2Mx (@ f)) * M) by A1, A5, MATRIX_0:30;
set LM = Line (((LineVec2Mx (@ f)) * M),1);
( i in Seg m & (Mx2Tran M) . f = Line (((LineVec2Mx (@ f)) * M),1) ) by A1, A2, Def3;
hence ((Mx2Tran M) . f) . i = ((LineVec2Mx (@ f)) * M) * (1,i) by A5, MATRIX_0:def 7
.= (Line ((LineVec2Mx (@ f)),1)) "*" (Col (M,i)) by A4, A3, A6, MATRIX_3:def 4
.= (@ f) "*" (Col (M,i)) by MATRIX15:25 ;
:: thesis: verum