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 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 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 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 (ColVec2Mx p) = len p by MATRIXR1:def 9;
A2: len (LineVec2Mx q) = 1 by MATRIXR1:def 10;
A3: len p > 0 ;
then A4: width (ColVec2Mx p) = 1 by MATRIXR1:def 9;
A5: width (LineVec2Mx q) = len q by MATRIXR1:def 10;

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

assume A6: M = (ColVec2Mx p) * (LineVec2Mx q) ; :: thesis: ( len M = len p & width M = len q & ( for i, j being Nat st [i,j] in Indices M holds
M * (i,j) = (p . i) * (q . j) ) )
then A7: len M = len (ColVec2Mx p) by A4, A2, MATRPROB:39;
thus ( len M = len p & width M = len q ) by A1, A4, A2, A5, A6, MATRPROB:39; :: thesis: for i, j being Nat st [i,j] in Indices M holds
M * (i,j) = (p . i) * (q . j)
A8: width M = width (LineVec2Mx q) by A4, A2, A6, MATRPROB:39;
thus for i, j being Nat st [i,j] in Indices M holds
M * (i,j) = (p . i) * (q . j) :: thesis: verum

proof

let i, j be Nat; :: thesis: ( [i,j] in Indices M implies M * (i,j) = (p . i) * (q . j) )
assume A9: [i,j] in Indices M ; :: thesis: M * (i,j) = (p . i) * (q . j)
A10: i in Seg (len M) by A9, MATRPROB:12;
then A11: i in dom p by A1, A7, FINSEQ_1:def 3;
j in Seg (width M) by A9, MATRPROB:12;
then A12: j in dom q by A5, A8, FINSEQ_1:def 3;
i in dom (ColVec2Mx p) by A7, A10, FINSEQ_1:def 3;
then A13: Line ((ColVec2Mx p),i) = (ColVec2Mx p) . i by MATRIX_0:60
.= <*(p . i)*> by A3, A11, MATRIXR1:def 9 ;
thus M * (i,j) = (Line ((ColVec2Mx p),i)) "*" (Col ((LineVec2Mx q),j)) by A4, A2, A6, A9, MATRPROB:39
.= <*(p . i)*> "*" <*(q . j)*> by A12, A13, Th20
.= Sum (mlt (<*(p . i)*>,<*(q . j)*>)) by RVSUM_1:def 16
.= Sum <*((p . i) * (q . j))*> by RVSUM_1:62
.= (p . i) * (q . j) by RVSUM_1:73 ; :: thesis: verum

end;

end;

assume that
A14: len M = len p and
A15: width M = len q and
A16: for i, j being 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 Nat st [i,j] in Indices M holds
M * (i,j) = (Line ((ColVec2Mx p),i)) "*" (Col ((LineVec2Mx q),j))

proof

let i, j be Nat; :: thesis: ( [i,j] in Indices M implies M * (i,j) = (Line ((ColVec2Mx p),i)) "*" (Col ((LineVec2Mx q),j)) )
assume A17: [i,j] in Indices M ; :: thesis: M * (i,j) = (Line ((ColVec2Mx p),i)) "*" (Col ((LineVec2Mx q),j))
j in Seg (width M) by A17, MATRPROB:12;
then A18: j in dom q by A15, FINSEQ_1:def 3;
A19: i in Seg (len M) by A17, MATRPROB:12;
then A20: i in dom (ColVec2Mx p) by A1, A14, FINSEQ_1:def 3;
i in dom p by A14, A19, FINSEQ_1:def 3;
then A21: <*(p . i)*> = (ColVec2Mx p) . i by A3, MATRIXR1:def 9
.= Line ((ColVec2Mx p),i) by A20, MATRIX_0:60 ;
thus M * (i,j) = (p . i) * (q . j) by A16, A17
.= Sum <*((p . i) * (q . j))*> by RVSUM_1:73
.= Sum (mlt (<*(p . i)*>,<*(q . j)*>)) by RVSUM_1:62
.= <*(p . i)*> "*" <*(q . j)*> by RVSUM_1:def 16
.= (Line ((ColVec2Mx p),i)) "*" (Col ((LineVec2Mx q),j)) by A18, A21, Th20 ; :: thesis: verum

end;

hence M = (ColVec2Mx p) * (LineVec2Mx q) by A1, A4, A2, A5, A14, A15, MATRPROB:39; :: thesis: verum