let p be FinSequence of REAL ; for j being Nat st j in dom p holds
Col ((LineVec2Mx p),j) = <*(p . j)*>
set M = LineVec2Mx p;
let j be Nat; ( j in dom p implies Col ((LineVec2Mx p),j) = <*(p . j)*> )
assume A1:
j in dom p
; 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 for k being Nat st k in dom (Col ((LineVec2Mx p),j)) holds
(Col ((LineVec2Mx p),j)) . k = <*(p . j)*> . klet k be
Nat;
( 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))
;
(Col ((LineVec2Mx p),j)) . k = <*(p . j)*> . kA6:
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, FINSEQ_1:def 8
;
verum end;
hence
Col ((LineVec2Mx p),j) = <*(p . j)*>
by A4, FINSEQ_1:13; verum