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
( Line (A,1) = <*a11,a12,a13*> & Line (A,2) = <*a21,a22,a23*> & Line (A,3) = <*a31,a32,a33*> )
let A be Matrix of 3,F_Real; :: thesis: ( A = <*<*a11,a12,a13*>,<*a21,a22,a23*>,<*a31,a32,a33*>*> implies ( Line (A,1) = <*a11,a12,a13*> & Line (A,2) = <*a21,a22,a23*> & Line (A,3) = <*a31,a32,a33*> ) )
assume A = <*<*a11,a12,a13*>,<*a21,a22,a23*>,<*a31,a32,a33*>*> ; :: thesis: ( Line (A,1) = <*a11,a12,a13*> & Line (A,2) = <*a21,a22,a23*> & Line (A,3) = <*a31,a32,a33*> )
then A1: ( A . 1 = <*a11,a12,a13*> & A . 2 = <*a21,a22,a23*> & A . 3 = <*a31,a32,a33*> ) ;
( 1 in Seg 3 & 2 in Seg 3 & 3 in Seg 3 ) by FINSEQ_1:1;
hence ( Line (A,1) = <*a11,a12,a13*> & Line (A,2) = <*a21,a22,a23*> & Line (A,3) = <*a31,a32,a33*> ) by A1, MATRIX_0:52; :: thesis: verum