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 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 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 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 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 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 Nat st i in dom M holds
Line (M,i) = (p . i) * q
thus for i being Nat st i in dom M holds
Line (M,i) = (p . i) * q :: thesis: verum

proof

let i be Nat; :: thesis: ( i in dom M implies Line (M,i) = (p . i) * q )
assume i in dom M ; :: thesis: Line (M,i) = (p . i) * q
then A2: i in Seg (len M) by FINSEQ_1:def 3;
A3: 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 j in dom (Line (M,i)) ; :: thesis: (Line (M,i)) . j = ((p . i) * q) . j
then j in Seg (len (Line (M,i))) by FINSEQ_1:def 3;
then A4: j in Seg (width M) by MATRIX_0:def 7;
then A5: [i,j] in Indices M by A2, MATRPROB:12;
thus (Line (M,i)) . j = M * (i,j) by A4, MATRIX_0:def 7
.= (p . i) * (q . j) by A1, A5, Th21
.= ((p . i) * q) . j by RVSUM_1:44 ; :: thesis: verum

end;

dom (Line (M,i)) = Seg (len (Line (M,i))) by FINSEQ_1:def 3
.= Seg (width M) by MATRIX_0:def 7
.= Seg (len q) by A1, Th21
.= dom q by FINSEQ_1:def 3
.= dom ((p . i) * q) by VALUED_1:def 5 ;
hence Line (M,i) = (p . i) * q by A3, FINSEQ_1:13; :: thesis: verum

end;

end;

assume that
A6: len M = len p and
A7: width M = len q and
A8: for i being Nat st i in dom M holds
Line (M,i) = (p . i) * q ; :: thesis: M = (ColVec2Mx p) * (LineVec2Mx q)
for i, j being Nat st [i,j] in Indices M holds
M * (i,j) = (p . i) * (q . j)

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 dom M by A9, MATRPROB:13;
j in Seg (width M) by A9, MATRPROB:12;
hence M * (i,j) = (Line (M,i)) . j by MATRIX_0:def 7
.= ((p . i) * q) . j by A8, A10
.= (p . i) * (q . j) by RVSUM_1:44 ;
:: thesis: verum

end;

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