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