let a11, a12, a13, a21, a22, a23, a31, a32, a33 be Element of F_Real; 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; ( 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*>*>
; ( 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 )
by FINSEQ_1:45;
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; verum