let p be FinSequence of REAL ; :: thesis: for j being Element of NAT st j in dom p holds
Col (LineVec2Mx p),j = <*(p . j)*>
set M = LineVec2Mx p;
let j be Element of 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_1:def 9;
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

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:3;
k >= 1 by A2, A4, A5, FINSEQ_1:3;
then A7: k = 1 by A6, XXREAL_0:1;
k in dom (LineVec2Mx p) by A3, A5, FINSEQ_3:31;
hence (Col (LineVec2Mx p),j) . k = (LineVec2Mx p) * k,j by MATRIX_1:def 9
.= p . j by A1, A7, MATRIXR1:def 10
.= <*(p . j)*> . k by A7, FINSEQ_1:def 8 ;
:: thesis: verum

end;

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