let n, m be Nat; :: thesis:
let f be n -element real-valued FinSequence; :: thesis:
let M be Matrix of n,m,F_Real; :: thesis:
assume A1: card (lines M) = 1 ; :: thesis:

per cases ;

suppose A2: n <> 0 ; :: thesis:

deffunc H₁( set ) -> Element of the carrier of F_Real = 0. F_Real;
A3: len M = n by A2, MATRIX13:1;
reconsider Sf = Sum f as Element of F_Real by XREAL_0:def 1;
set Mf = (Mx2Tran M) . f;
A4: len ((Mx2Tran M) . f) = m by CARD_1:def 7;
A5: len f = n by CARD_1:def 7;
set V = m -VectSp_over F_Real;
consider x being object such that
A6: lines M = {x} by A1, CARD_2:42;
x in lines M by A6, TARSKI:def 1;
then consider j being object such that
A7: j in dom M and
A8: M . j = x by FUNCT_1:def 3;
reconsider j = j as Nat by A7;
A9: width M = m by A2, MATRIX13:1;
then reconsider LMj = Line (M,j) as Element of (m -VectSp_over F_Real) by MATRIX13:102;
consider L being Function of the carrier of (m -VectSp_over F_Real), the carrier of F_Real such that
A10: L . LMj = 1. F_Real and
A11: for z being Element of (m -VectSp_over F_Real) st z <> LMj holds
L . z = H₁(z) from FUNCT_2:sch 6();
reconsider L = L as Element of Funcs ( the carrier of (m -VectSp_over F_Real), the carrier of F_Real) by FUNCT_2:8;
A12: x = Line (M,j) by A7, A8, MATRIX_0:60;

A13: now :: thesis:

let z be Vector of (m -VectSp_over F_Real); :: thesis:
assume A14: not z in lines M ; :: thesis:
z <> LMj by A6, A12, A14, TARSKI:def 1;
hence L . z = 0. F_Real by A11; :: thesis:

end;

A15: len (Sf * (Line (M,j))) = m by A9, CARD_1:def 7;

A16: now :: thesis:

len (@ f) = n by CARD_1:def 7;
then reconsider F = @ f as Element of n -tuples_on the carrier of F_Real by FINSEQ_2:92;
let w be Nat; :: thesis:
set Mjw = M * (j,w);
assume A17: ( 1 <= w & w <= m ) ; :: thesis:
then A18: w in dom (Sf * (Line (M,j))) by A15, FINSEQ_3:25;
A19: w in Seg m by A17;
then A20: (Line (M,j)) . w = M * (j,w) by A9, MATRIX_0:def 7;

A21: now :: thesis:

let z be Nat; :: thesis:
assume A22: ( 1 <= z & z <= n ) ; :: thesis:
then A23: z in Seg n ;
then A24: Line (M,z) in lines M by MATRIX13:103;
z in dom M by A3, A22, FINSEQ_3:25;
hence (Col (M,w)) . z = M * (z,w) by MATRIX_0:def 8
.= (Line (M,z)) . w by A9, A19, MATRIX_0:def 7
.= M * (j,w) by A6, A12, A20, A24, TARSKI:def 1
.= (n |-> (M * (j,w))) . z by A23, FINSEQ_2:57 ;
:: thesis:

end;

( len (Col (M,w)) = n & len (n |-> (M * (j,w))) = n ) by A3, CARD_1:def 7;
then A25: Col (M,w) = n |-> (M * (j,w)) by A21;
thus ((Mx2Tran M) . f) . w = (@ f) "*" (Col (M,w)) by A2, A17, MATRTOP1:18
.= Sum (mlt ((@ f),(Col (M,w)))) by FVSUM_1:def 9
.= Sum ((M * (j,w)) * F) by A25, FVSUM_1:66
.= (M * (j,w)) * (Sum (@ f)) by FVSUM_1:73
.= (M * (j,w)) * Sf by MATRPROB:36
.= (Sf * (Line (M,j))) . w by A18, A20, FVSUM_1:50 ; :: thesis:

end;

reconsider L = L as Linear_Combination of m -VectSp_over F_Real by A13, VECTSP_6:def 1;
Carrier L c= {LMj}

proof

let x be object ; :: according to TARSKI:def 3 :: thesis:
assume A26: x in Carrier L ; :: thesis:
L . x <> 0. F_Real by A26, VECTSP_6:2;
then x = LMj by A11, A26;
hence x in {LMj} by TARSKI:def 1; :: thesis:

end;

then reconsider L = L as Linear_Combination of lines M by A6, A12, VECTSP_6:def 4;
A27: Sum L = (1. F_Real) * LMj by A6, A12, A10, VECTSP_6:17
.= LMj ;
reconsider SfL = Sf * L as Linear_Combination of lines M by VECTSP_6:31;
take SfL ; :: thesis:
Sum SfL = Sf * (Sum L) by VECTSP_6:45
.= Sf * (Line (M,j)) by A9, A27, MATRIX13:102 ;
hence Sum SfL = (Mx2Tran M) . f by A15, A4, A16, FINSEQ_1:14; :: thesis:
let w be Nat; :: thesis:
assume A28: w in Seg n ; :: thesis:
Line (M,w) in lines M by A28, MATRIX13:103;
then A29: Line (M,w) = LMj by A6, A12, TARSKI:def 1;
thus Sum f = Sf * 1
.= Sf * (1. F_Real)
.= SfL . (Line (M,w)) by A10, A29, VECTSP_6:def 9 ; :: thesis:
thus M " {(Line (M,w))} = dom M by A6, A12, A29, RELAT_1:134
.= dom f by A3, A5, FINSEQ_3:29 ; :: thesis:

end;

suppose A30: n = 0 ; :: thesis:

reconsider L = ZeroLC (m -VectSp_over F_Real) as Linear_Combination of lines M by VECTSP_6:5;
take L ; :: thesis:
thus Sum L = 0. (m -VectSp_over F_Real) by VECTSP_6:15
.= 0. (TOP-REAL m) by Lm2
.= (Mx2Tran M) . f by A30, MATRTOP1:def 3 ; :: thesis:
thus for k being Nat st k in Seg n holds
( L . (Line (M,k)) = Sum f & M " {(Line (M,k))} = dom f ) by A30; :: thesis:

end;

end;