let p be non empty FinSequence of REAL ; :: thesis: for q being FinSequence of REAL
for M being Matrix of REAL holds
( M = (ColVec2Mx p) * (LineVec2Mx q) iff ( len M = len p & width M = len q & ( for i being Element of NAT st i in dom M holds
Line M,i = (p . i) * q ) ) )
let q be FinSequence of REAL ; :: thesis: for M being Matrix of REAL holds
( M = (ColVec2Mx p) * (LineVec2Mx q) iff ( len M = len p & width M = len q & ( for i being Element of NAT st i in dom M holds
Line M,i = (p . i) * q ) ) )
let M be Matrix of REAL ; :: thesis: ( M = (ColVec2Mx p) * (LineVec2Mx q) iff ( len M = len p & width M = len q & ( for i being Element of NAT st i in dom M holds
Line M,i = (p . i) * q ) ) )
set M1 = ColVec2Mx p;
set M2 = LineVec2Mx q;

hereby :: thesis: ( len M = len p & width M = len q & ( for i being Element of NAT st i in dom M holds
Line M,i = (p . i) * q ) implies M = (ColVec2Mx p) * (LineVec2Mx q) )

assume A1: M = (ColVec2Mx p) * (LineVec2Mx q) ; :: thesis: ( len M = len p & width M = len q & ( for i being Element of NAT st i in dom M holds
Line M,i = (p . i) * q ) )
hence ( len M = len p & width M = len q ) by Th21; :: thesis: for i being Element of NAT st i in dom M holds
Line M,i = (p . i) * q
thus for i being Element of NAT st i in dom M holds
Line M,i = (p . i) * q :: thesis: verum

proof

let i be Element of NAT ; :: thesis: ( i in dom M implies Line M,i = (p . i) * q )
assume A2: i in dom M ; :: thesis: Line M,i = (p . i) * q
A3: i in Seg (len M) by A2, FINSEQ_1:def 3;
A4: dom (Line M,i) = Seg (len (Line M,i)) by FINSEQ_1:def 3
.= Seg (width M) by MATRIX_1:def 8
.= Seg (len q) by A1, Th21
.= dom q by FINSEQ_1:def 3
.= dom ((p . i) * q) by VALUED_1:def 5 ;
for j being Nat st j in dom (Line M,i) holds
(Line M,i) . j = ((p . i) * q) . j

proof

let j be Nat; :: thesis: ( j in dom (Line M,i) implies (Line M,i) . j = ((p . i) * q) . j )
assume A5: j in dom (Line M,i) ; :: thesis: (Line M,i) . j = ((p . i) * q) . j
A6: j in NAT by ORDINAL1:def 13;
j in Seg (len (Line M,i)) by A5, FINSEQ_1:def 3;
then A7: j in Seg (width M) by MATRIX_1:def 8;
then A8: [i,j] in Indices M by A3, MATRPROB:12;
thus (Line M,i) . j = M * i,j by A7, MATRIX_1:def 8
.= (p . i) * (q . j) by A1, A6, A8, Th21
.= ((p . i) * q) . j by RVSUM_1:66 ; :: thesis: verum

end;

hence Line M,i = (p . i) * q by A4, FINSEQ_1:17; :: thesis: verum

end;

end;

assume A9: ( len M = len p & width M = len q & ( for i being Element of NAT st i in dom M holds
Line M,i = (p . i) * q ) ) ; :: thesis: M = (ColVec2Mx p) * (LineVec2Mx q)
for i, j being Element of NAT st [i,j] in Indices M holds
M * i,j = (p . i) * (q . j)

proof

let i, j be Element of NAT ; :: thesis: ( [i,j] in Indices M implies M * i,j = (p . i) * (q . j) )
assume A10: [i,j] in Indices M ; :: thesis: M * i,j = (p . i) * (q . j)
A11: ( i in dom M & j in dom (M . i) ) by A10, MATRPROB:13;
j in Seg (width M) by A10, MATRPROB:12;
hence M * i,j = (Line M,i) . j by MATRIX_1:def 8
.= ((p . i) * q) . j by A9, A11
.= (p . i) * (q . j) by RVSUM_1:66 ;
:: thesis: verum

end;

hence M = (ColVec2Mx p) * (LineVec2Mx q) by A9, Th21; :: thesis: verum