let p be FinSequence of 1 -tuples_on REAL; :: thesis: ( len p = 3 implies ColVec2Mx (M2F p) = p )
assume A1: len p = 3 ; :: thesis: ColVec2Mx (M2F p) = p
then A2: M2F p = <*((p . 1) . 1),((p . 2) . 1),((p . 3) . 1)*> by ANPROJ_8:def 2;
then A3: len (M2F p) = 3 by FINSEQ_1:45;
A4: len (M2F p) > 0 by A2, FINSEQ_1:45;
then A5: len (ColVec2Mx (M2F p)) = len (M2F p) by MATRIXR1:def 9
.= 3 by A2, FINSEQ_1:45 ;
( width (ColVec2Mx (M2F p)) = 1 & ColVec2Mx (M2F p) is Matrix of REAL ) by A4, MATRIXR1:def 9;
then A6: ColVec2Mx (M2F p) is Matrix of 3,1,F_Real by A5, MATRIX_0:20;
set A = ColVec2Mx (M2F p);
ColVec2Mx (M2F p) = <*<*((ColVec2Mx (M2F p)) * (1,1))*>,<*((ColVec2Mx (M2F p)) * (2,1))*>,<*((ColVec2Mx (M2F p)) * (3,1))*>*> by A6, Th27;
then A7: ( (ColVec2Mx (M2F p)) . 1 = <*((ColVec2Mx (M2F p)) * (1,1))*> & (ColVec2Mx (M2F p)) . 2 = <*((ColVec2Mx (M2F p)) * (2,1))*> & (ColVec2Mx (M2F p)) . 3 = <*((ColVec2Mx (M2F p)) * (3,1))*> ) by FINSEQ_1:45;
dom (M2F p) = Seg 3 by A3, FINSEQ_1:def 3;
then ( 1 in dom (M2F p) & 2 in dom (M2F p) & 3 in dom (M2F p) ) by FINSEQ_1:1;
then ( (ColVec2Mx (M2F p)) . 1 = <*((M2F p) . 1)*> & (ColVec2Mx (M2F p)) . 2 = <*((M2F p) . 2)*> & (ColVec2Mx (M2F p)) . 3 = <*((M2F p) . 3)*> ) by A4, MATRIXR1:def 9;
then ColVec2Mx (M2F p) = <*<*((M2F p) . 1)*>,<*((M2F p) . 2)*>,<*((M2F p) . 3)*>*> by A6, Th27, A7
.= F2M (M2F p) by A3, ANPROJ_8:def 1
.= p by A1, ANPROJ_8:85 ;
hence ColVec2Mx (M2F p) = p ; :: thesis: verum