let D be non empty set ; :: thesis: for pf being FinSequence of D
for pr being Element of REAL 3 st pf = pr holds
MXR2MXF (ColVec2Mx pr) = <*pf*> @
let pf be FinSequence of D; :: thesis: for pr being Element of REAL 3 st pf = pr holds
MXR2MXF (ColVec2Mx pr) = <*pf*> @
let pr be Element of REAL 3; :: thesis: ( pf = pr implies MXR2MXF (ColVec2Mx pr) = <*pf*> @ )
assume A1: pf = pr ; :: thesis: MXR2MXF (ColVec2Mx pr) = <*pf*> @
set M1 = MXR2MXF (ColVec2Mx pr);
set M2 = ColVec2Mx pr;
A2: MXR2MXF (ColVec2Mx pr) = ColVec2Mx pr by MATRIXR1:def 1;
pr in REAL 3 ;
then A3: pr in 3 -tuples_on REAL by EUCLID:def 1;
then A4: len pr = 3 by FINSEQ_2:133;
A5: ( len (ColVec2Mx pr) = len pr & width (ColVec2Mx pr) = 1 & ( for j being Nat st j in dom pr holds
(ColVec2Mx pr) . j = <*(pr . j)*> ) ) by A4, MATRIXR1:def 9;

now :: thesis: ( len (ColVec2Mx pr) = len (<*pf*> @) & ( for k being Nat st 1 <= k & k <= len (ColVec2Mx pr) holds
(ColVec2Mx pr) . k = (<*pf*> @) . k ) )

A6: width <*pf*> = len pr by A1, MATRIX_0:23;
hence len (ColVec2Mx pr) = len (<*pf*> @) by A5, MATRIX_0:def 6; :: thesis: for k being Nat st 1 <= k & k <= len (ColVec2Mx pr) holds
(ColVec2Mx pr) . k = (<*pf*> @) . k
thus for k being Nat st 1 <= k & k <= len (ColVec2Mx pr) holds
(ColVec2Mx pr) . k = (<*pf*> @) . k :: thesis: verum

proof

let k be Nat; :: thesis: ( 1 <= k & k <= len (ColVec2Mx pr) implies (ColVec2Mx pr) . k = (<*pf*> @) . k )
assume that
A7: 1 <= k and
A8: k <= len (ColVec2Mx pr) ; :: thesis: (ColVec2Mx pr) . k = (<*pf*> @) . k
A9: k in Seg (len pr) by A5, A7, A8, FINSEQ_1:1;
then A10: k in dom pr by FINSEQ_1:def 3;
A11: len <*pf*> = 1 by MATRIX_0:23;
A12: width <*pf*> = 3 by A6, A3, FINSEQ_2:133;
Seg (len (<*pf*> @)) = Seg (len pr) by A6, MATRIX_0:def 6;
then dom (<*pf*> @) = Seg (len pr) by FINSEQ_1:def 3
.= dom pr by FINSEQ_1:def 3 ;
then A13: k in dom (<*pf*> @) by A9, FINSEQ_1:def 3;
then A14: (<*pf*> @) . k = Line ((<*pf*> @),k) by MATRIX_0:60
.= Col (((<*pf*> @) @),k) by A13, MATRIX_0:58
.= Col (<*pf*>,k) by A12, A11, MATRIX_0:57
.= <*(pf . k)*> by A10, A1, Th59 ;
k in dom pr by A9, FINSEQ_1:def 3;
hence (ColVec2Mx pr) . k = (<*pf*> @) . k by A4, MATRIXR1:def 9, A1, A14; :: thesis: verum

end;

end;

hence MXR2MXF (ColVec2Mx pr) = <*pf*> @ by A2, FINSEQ_1:def 18; :: thesis: verum