let a11, a12, a13, a21, a22, a23, a31, a32, a33 be Element of F_Real; :: thesis: for A being Matrix of 3,F_Real st A = <*<*a11,a12,a13*>,<*a21,a22,a23*>,<*a31,a32,a33*>*> holds
( Col (A,1) = <*a11,a21,a31*> & Col (A,2) = <*a12,a22,a32*> & Col (A,3) = <*a13,a23,a33*> )
let A be Matrix of 3,F_Real; :: thesis: ( A = <*<*a11,a12,a13*>,<*a21,a22,a23*>,<*a31,a32,a33*>*> implies ( Col (A,1) = <*a11,a21,a31*> & Col (A,2) = <*a12,a22,a32*> & Col (A,3) = <*a13,a23,a33*> ) )
assume A1: A = <*<*a11,a12,a13*>,<*a21,a22,a23*>,<*a31,a32,a33*>*> ; :: thesis: ( Col (A,1) = <*a11,a21,a31*> & Col (A,2) = <*a12,a22,a32*> & Col (A,3) = <*a13,a23,a33*> )
( |[a11,a12,a13]| is Point of (TOP-REAL 3) & |[a21,a22,a23]| is Point of (TOP-REAL 3) & |[a31,a32,a33]| is Point of (TOP-REAL 3) ) ;
then reconsider p = <*a11,a12,a13*>, q = <*a21,a22,a23*>, r = <*a31,a32,a33*> as Point of (TOP-REAL 3) ;
( p . 1 = a11 & p . 2 = a12 & p . 3 = a13 & q . 1 = a21 & q . 2 = a22 & q . 3 = a23 & r . 1 = a31 & r . 2 = a32 & r . 3 = a33 ) ;
then A2: ( p `1 = a11 & p `2 = a12 & p `3 = a13 & q `1 = a21 & q `2 = a22 & q `3 = a23 & r `1 = a31 & r `2 = a32 & r `3 = a33 ) by EUCLID_5:def 1, EUCLID_5:def 2, EUCLID_5:def 3;
A @ = <*<*(p `1),(q `1),(r `1)*>,<*(p `2),(q `2),(r `2)*>,<*(p `3),(q `3),(r `3)*>*> by A1, ANPROJ_8:23;
then A3: ( Line ((A @),1) = <*a11,a21,a31*> & Line ((A @),2) = <*a12,a22,a32*> & Line ((A @),3) = <*a13,a23,a33*> ) by A2, Th05;
A4: width A = 3 by MATRIX_0:24;
( 1 in Seg 3 & 2 in Seg 3 & 3 in Seg 3 ) by FINSEQ_1:1;
hence ( Col (A,1) = <*a11,a21,a31*> & Col (A,2) = <*a12,a22,a32*> & Col (A,3) = <*a13,a23,a33*> ) by A3, A4, MATRIX_0:59; :: thesis: verum