let p be FinSequence of REAL ; :: thesis: for j being Nat st j in dom p holds
Col ((LineVec2Mx p),j) = <*(p . j)*>
set M = LineVec2Mx p;
let j be Nat; :: thesis: ( j in dom p implies Col ((LineVec2Mx p),j) = <*(p . j)*> )
assume A1: j in dom p ; :: thesis: Col ((LineVec2Mx p),j) = <*(p . j)*>
A2: dom <*(p . j)*> = Seg 1 by FINSEQ_1:def 8;
A3: len (Col ((LineVec2Mx p),j)) = len (LineVec2Mx p) by MATRIX_0:def 8;
then len (Col ((LineVec2Mx p),j)) = 1 by MATRIXR1:def 10;
then A4: dom (Col ((LineVec2Mx p),j)) = dom <*(p . j)*> by A2, FINSEQ_1:def 3;

now :: thesis: for k being Nat st k in dom (Col ((LineVec2Mx p),j)) holds
(Col ((LineVec2Mx p),j)) . k = <*(p . j)*> . k

let k be Nat; :: thesis: ( k in dom (Col ((LineVec2Mx p),j)) implies (Col ((LineVec2Mx p),j)) . k = <*(p . j)*> . k )
assume A5: k in dom (Col ((LineVec2Mx p),j)) ; :: thesis: (Col ((LineVec2Mx p),j)) . k = <*(p . j)*> . k
A6: k <= 1 by A2, A4, A5, FINSEQ_1:1;
k >= 1 by A2, A4, A5, FINSEQ_1:1;
then A7: k = 1 by A6, XXREAL_0:1;
k in dom (LineVec2Mx p) by A3, A5, FINSEQ_3:29;
hence (Col ((LineVec2Mx p),j)) . k = (LineVec2Mx p) * (k,j) by MATRIX_0:def 8
.= p . j by A1, A7, MATRIXR1:def 10
.= <*(p . j)*> . k by A7 ;
:: thesis: verum

end;

hence Col ((LineVec2Mx p),j) = <*(p . j)*> by A4, FINSEQ_1:13; :: thesis: verum