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, j being Element of NAT st [i,j] in Indices M holds
M * i,j = (p . i) * (q . j) ) ) )
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, j being Element of NAT st [i,j] in Indices M holds
M * i,j = (p . i) * (q . j) ) ) )
let M be Matrix of REAL ; :: thesis: ( M = (ColVec2Mx p) * (LineVec2Mx q) iff ( len M = len p & width M = len q & ( for i, j being Element of NAT st [i,j] in Indices M holds
M * i,j = (p . i) * (q . j) ) ) )
set M1 = ColVec2Mx p;
set M2 = LineVec2Mx q;
A1: len p > 0 ;
then A2: ( len (ColVec2Mx p) = len p & width (ColVec2Mx p) = 1 & ( for j being Element of NAT st j in dom p holds
(ColVec2Mx p) . j = <*(p . j)*> ) ) by MATRIXR1:def 9;
A3: ( len (LineVec2Mx q) = 1 & width (LineVec2Mx q) = len q & ( for j being Element of NAT st j in dom q holds
(LineVec2Mx q) * 1,j = q . j ) ) by MATRIXR1:def 10;

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

assume A4: M = (ColVec2Mx p) * (LineVec2Mx q) ; :: thesis: ( len M = len p & width M = len q & ( for i, j being Element of NAT st [i,j] in Indices M holds
M * i,j = (p . i) * (q . j) ) )
then A5: ( len M = len (ColVec2Mx p) & width M = width (LineVec2Mx q) & ( for i, j being Element of NAT st [i,j] in Indices M holds
M * i,j = (Line (ColVec2Mx p),i) "*" (Col (LineVec2Mx q),j) ) ) by A2, A3, MATRPROB:39;
thus ( len M = len p & width M = len q ) by A2, A3, A4, MATRPROB:39; :: thesis: for i, j being Element of NAT st [i,j] in Indices M holds
M * i,j = (p . i) * (q . j)
thus for i, j being Element of NAT st [i,j] in Indices M holds
M * i,j = (p . i) * (q . j) :: thesis: verum

proof

let i, j be Element of NAT ; :: thesis: ( [i,j] in Indices M implies M * i,j = (p . i) * (q . j) )
assume A6: [i,j] in Indices M ; :: thesis: M * i,j = (p . i) * (q . j)
A7: ( i in Seg (len M) & j in Seg (width M) ) by A6, MATRPROB:12;
then A8: i in dom (ColVec2Mx p) by A5, FINSEQ_1:def 3;
A9: ( i in dom p & j in dom q ) by A2, A3, A5, A7, FINSEQ_1:def 3;
A10: Line (ColVec2Mx p),i = (ColVec2Mx p) . i by A8, MATRIX_2:18
.= <*(p . i)*> by A1, A9, MATRIXR1:def 9 ;
thus M * i,j = (Line (ColVec2Mx p),i) "*" (Col (LineVec2Mx q),j) by A2, A3, A4, A6, MATRPROB:39
.= <*(p . i)*> "*" <*(q . j)*> by A9, A10, Th20
.= Sum (mlt <*(p . i)*>,<*(q . j)*>) by EUCLID_2:def 1
.= Sum <*((p . i) * (q . j))*> by RVSUM_1:89
.= (p . i) * (q . j) by RVSUM_1:103 ; :: thesis: verum

end;

end;

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

proof

let i, j be Element of NAT ; :: thesis: ( [i,j] in Indices M implies M * i,j = (Line (ColVec2Mx p),i) "*" (Col (LineVec2Mx q),j) )
assume A12: [i,j] in Indices M ; :: thesis: M * i,j = (Line (ColVec2Mx p),i) "*" (Col (LineVec2Mx q),j)
A13: ( i in Seg (len M) & j in Seg (width M) ) by A12, MATRPROB:12;
then A14: i in dom (ColVec2Mx p) by A2, A11, FINSEQ_1:def 3;
A15: ( i in dom p & j in dom q ) by A11, A13, FINSEQ_1:def 3;
then A16: <*(p . i)*> = (ColVec2Mx p) . i by A1, MATRIXR1:def 9
.= Line (ColVec2Mx p),i by A14, MATRIX_2:18 ;
thus M * i,j = (p . i) * (q . j) by A11, A12
.= Sum <*((p . i) * (q . j))*> by RVSUM_1:103
.= Sum (mlt <*(p . i)*>,<*(q . j)*>) by RVSUM_1:89
.= <*(p . i)*> "*" <*(q . j)*> by EUCLID_2:def 1
.= (Line (ColVec2Mx p),i) "*" (Col (LineVec2Mx q),j) by A15, A16, Th20 ; :: thesis: verum

end;

hence M = (ColVec2Mx p) * (LineVec2Mx q) by A2, A3, A11, MATRPROB:39; :: thesis: verum