let p, q, r be Point of (TOP-REAL 3); :: thesis: for PQR being Matrix of 3,F_Real st PQR = <*<*(p `1),(p `2),(p `3)*>,<*(q `1),(q `2),(q `3)*>,<*(r `1),(r `2),(r `3)*>*> holds
( Line (PQR,1) = p & Line (PQR,2) = q & Line (PQR,3) = r )
let PQR be Matrix of 3,F_Real; :: thesis: ( PQR = <*<*(p `1),(p `2),(p `3)*>,<*(q `1),(q `2),(q `3)*>,<*(r `1),(r `2),(r `3)*>*> implies ( Line (PQR,1) = p & Line (PQR,2) = q & Line (PQR,3) = r ) )
assume A1: PQR = <*<*(p `1),(p `2),(p `3)*>,<*(q `1),(q `2),(q `3)*>,<*(r `1),(r `2),(r `3)*>*> ; :: thesis: ( Line (PQR,1) = p & Line (PQR,2) = q & Line (PQR,3) = r )
1 in Seg 3 by FINSEQ_1:1;
hence Line (PQR,1) = PQR . 1 by MATRIX_0:52
.= <*(p `1),(p `2),(p `3)*> by A1
.= p by EUCLID_5:3 ;
:: thesis: ( Line (PQR,2) = q & Line (PQR,3) = r )
2 in Seg 3 by FINSEQ_1:1;
hence Line (PQR,2) = PQR . 2 by MATRIX_0:52
.= <*(q `1),(q `2),(q `3)*> by A1
.= q by EUCLID_5:3 ;
:: thesis: Line (PQR,3) = r
3 in Seg 3 by FINSEQ_1:1;
hence Line (PQR,3) = PQR . 3 by MATRIX_0:52
.= <*(r `1),(r `2),(r `3)*> by A1
.= r by EUCLID_5:3 ;
:: thesis: verum