let p, q, r be Point of (TOP-REAL 3); for M being Matrix of 3,F_Real st M = <*p,q,r*> holds
( M * (1,1) = p `1 & M * (1,2) = p `2 & M * (1,3) = p `3 & M * (2,1) = q `1 & M * (2,2) = q `2 & M * (2,3) = q `3 & M * (3,1) = r `1 & M * (3,2) = r `2 & M * (3,3) = r `3 )
let M be Matrix of 3,F_Real; ( M = <*p,q,r*> implies ( M * (1,1) = p `1 & M * (1,2) = p `2 & M * (1,3) = p `3 & M * (2,1) = q `1 & M * (2,2) = q `2 & M * (2,3) = q `3 & M * (3,1) = r `1 & M * (3,2) = r `2 & M * (3,3) = r `3 ) )
assume
M = <*p,q,r*>
; ( M * (1,1) = p `1 & M * (1,2) = p `2 & M * (1,3) = p `3 & M * (2,1) = q `1 & M * (2,2) = q `2 & M * (2,3) = q `3 & M * (3,1) = r `1 & M * (3,2) = r `2 & M * (3,3) = r `3 )
then
( M . 1 = p & M . 2 = q & M . 3 = r )
by FINSEQ_1:45;
then A1:
( M . 1 = <*(p `1),(p `2),(p `3)*> & M . 2 = <*(q `1),(q `2),(q `3)*> & M . 3 = <*(r `1),(r `2),(r `3)*> )
by EUCLID_5:3;
A2:
( [1,1] in Indices M & [1,2] in Indices M & [1,3] in Indices M & [2,1] in Indices M & [2,2] in Indices M & [2,3] in Indices M & [3,1] in Indices M & [3,2] in Indices M & [3,3] in Indices M )
by MATRIX_0:24, Th1;
then
ex s being FinSequence of F_Real st
( s = M . 1 & M * (1,1) = s . 1 )
by MATRIX_0:def 5;
hence
M * (1,1) = p `1
by A1, FINSEQ_1:45; ( M * (1,2) = p `2 & M * (1,3) = p `3 & M * (2,1) = q `1 & M * (2,2) = q `2 & M * (2,3) = q `3 & M * (3,1) = r `1 & M * (3,2) = r `2 & M * (3,3) = r `3 )
ex s being FinSequence of F_Real st
( s = M . 1 & M * (1,2) = s . 2 )
by A2, MATRIX_0:def 5;
hence
M * (1,2) = p `2
by A1, FINSEQ_1:45; ( M * (1,3) = p `3 & M * (2,1) = q `1 & M * (2,2) = q `2 & M * (2,3) = q `3 & M * (3,1) = r `1 & M * (3,2) = r `2 & M * (3,3) = r `3 )
ex s being FinSequence of F_Real st
( s = M . 1 & M * (1,3) = s . 3 )
by A2, MATRIX_0:def 5;
hence
M * (1,3) = p `3
by A1, FINSEQ_1:45; ( M * (2,1) = q `1 & M * (2,2) = q `2 & M * (2,3) = q `3 & M * (3,1) = r `1 & M * (3,2) = r `2 & M * (3,3) = r `3 )
ex s being FinSequence of F_Real st
( s = M . 2 & M * (2,1) = s . 1 )
by A2, MATRIX_0:def 5;
hence
M * (2,1) = q `1
by A1, FINSEQ_1:45; ( M * (2,2) = q `2 & M * (2,3) = q `3 & M * (3,1) = r `1 & M * (3,2) = r `2 & M * (3,3) = r `3 )
ex s being FinSequence of F_Real st
( s = M . 2 & M * (2,2) = s . 2 )
by A2, MATRIX_0:def 5;
hence
M * (2,2) = q `2
by A1, FINSEQ_1:45; ( M * (2,3) = q `3 & M * (3,1) = r `1 & M * (3,2) = r `2 & M * (3,3) = r `3 )
ex s being FinSequence of F_Real st
( s = M . 2 & M * (2,3) = s . 3 )
by A2, MATRIX_0:def 5;
hence
M * (2,3) = q `3
by A1, FINSEQ_1:45; ( M * (3,1) = r `1 & M * (3,2) = r `2 & M * (3,3) = r `3 )
ex s being FinSequence of F_Real st
( s = M . 3 & M * (3,1) = s . 1 )
by A2, MATRIX_0:def 5;
hence
M * (3,1) = r `1
by A1, FINSEQ_1:45; ( M * (3,2) = r `2 & M * (3,3) = r `3 )
ex s being FinSequence of F_Real st
( s = M . 3 & M * (3,2) = s . 2 )
by A2, MATRIX_0:def 5;
hence
M * (3,2) = r `2
by A1, FINSEQ_1:45; M * (3,3) = r `3
ex s being FinSequence of F_Real st
( s = M . 3 & M * (3,3) = s . 3 )
by A2, MATRIX_0:def 5;
hence
M * (3,3) = r `3
by A1, FINSEQ_1:45; verum