let M be Matrix of 3,F_Real; for p1, p2, p3, q1, q2, q3, r1, r2, r3 being Real st M = <*<*p1,q1,r1*>,<*p2,q2,r2*>,<*p3,q3,r3*>*> holds
( M * (1,1) = p1 & M * (1,2) = q1 & M * (1,3) = r1 & M * (2,1) = p2 & M * (2,2) = q2 & M * (2,3) = r2 & M * (3,1) = p3 & M * (3,2) = q3 & M * (3,3) = r3 )
let p1, p2, p3, q1, q2, q3, r1, r2, r3 be Real; ( M = <*<*p1,q1,r1*>,<*p2,q2,r2*>,<*p3,q3,r3*>*> implies ( M * (1,1) = p1 & M * (1,2) = q1 & M * (1,3) = r1 & M * (2,1) = p2 & M * (2,2) = q2 & M * (2,3) = r2 & M * (3,1) = p3 & M * (3,2) = q3 & M * (3,3) = r3 ) )
assume
M = <*<*p1,q1,r1*>,<*p2,q2,r2*>,<*p3,q3,r3*>*>
; ( M * (1,1) = p1 & M * (1,2) = q1 & M * (1,3) = r1 & M * (2,1) = p2 & M * (2,2) = q2 & M * (2,3) = r2 & M * (3,1) = p3 & M * (3,2) = q3 & M * (3,3) = r3 )
then A1:
( M . 1 = <*p1,q1,r1*> & M . 2 = <*p2,q2,r2*> & M . 3 = <*p3,q3,r3*> )
by FINSEQ_1:45;
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) = p1
by A1, FINSEQ_1:45; ( M * (1,2) = q1 & M * (1,3) = r1 & M * (2,1) = p2 & M * (2,2) = q2 & M * (2,3) = r2 & M * (3,1) = p3 & M * (3,2) = q3 & M * (3,3) = r3 )
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) = q1
by A1, FINSEQ_1:45; ( M * (1,3) = r1 & M * (2,1) = p2 & M * (2,2) = q2 & M * (2,3) = r2 & M * (3,1) = p3 & M * (3,2) = q3 & M * (3,3) = r3 )
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) = r1
by A1, FINSEQ_1:45; ( M * (2,1) = p2 & M * (2,2) = q2 & M * (2,3) = r2 & M * (3,1) = p3 & M * (3,2) = q3 & M * (3,3) = r3 )
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) = p2
by A1, FINSEQ_1:45; ( M * (2,2) = q2 & M * (2,3) = r2 & M * (3,1) = p3 & M * (3,2) = q3 & M * (3,3) = r3 )
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) = q2
by A1, FINSEQ_1:45; ( M * (2,3) = r2 & M * (3,1) = p3 & M * (3,2) = q3 & M * (3,3) = r3 )
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) = r2
by A1, FINSEQ_1:45; ( M * (3,1) = p3 & M * (3,2) = q3 & M * (3,3) = r3 )
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) = p3
by A1, FINSEQ_1:45; ( M * (3,2) = q3 & M * (3,3) = r3 )
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) = q3
by A1, FINSEQ_1:45; M * (3,3) = r3
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) = r3
by A1, FINSEQ_1:45; verum