let K be Field; :: thesis: for a, b, c, d, e, f, g, h, i being Element of K
for M being Matrix of 3,K st M = <*<*a,b,c*>,<*d,e,f*>,<*g,h,i*>*> holds
( a = M * (1,1) & b = M * (1,2) & c = M * (1,3) & d = M * (2,1) & e = M * (2,2) & f = M * (2,3) & g = M * (3,1) & h = M * (3,2) & i = M * (3,3) )
let a, b, c, d, e, f, g, h, i be Element of K; :: thesis: for M being Matrix of 3,K st M = <*<*a,b,c*>,<*d,e,f*>,<*g,h,i*>*> holds
( a = M * (1,1) & b = M * (1,2) & c = M * (1,3) & d = M * (2,1) & e = M * (2,2) & f = M * (2,3) & g = M * (3,1) & h = M * (3,2) & i = M * (3,3) )
let M be Matrix of 3,K; :: thesis: ( M = <*<*a,b,c*>,<*d,e,f*>,<*g,h,i*>*> implies ( a = M * (1,1) & b = M * (1,2) & c = M * (1,3) & d = M * (2,1) & e = M * (2,2) & f = M * (2,3) & g = M * (3,1) & h = M * (3,2) & i = M * (3,3) ) )
assume M = <*<*a,b,c*>,<*d,e,f*>,<*g,h,i*>*> ; :: thesis: ( a = M * (1,1) & b = M * (1,2) & c = M * (1,3) & d = M * (2,1) & e = M * (2,2) & f = M * (2,3) & g = M * (3,1) & h = M * (3,2) & i = M * (3,3) )
then A1: ( M . 1 = <*a,b,c*> & M . 2 = <*d,e,f*> & M . 3 = <*g,h,i*> ) 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, ANPROJ_8:1;
then ex s being FinSequence of K st
( s = M . 1 & M * (1,1) = s . 1 ) by MATRIX_0:def 5;
hence M * (1,1) = a by A1, FINSEQ_1:45; :: thesis: ( b = M * (1,2) & c = M * (1,3) & d = M * (2,1) & e = M * (2,2) & f = M * (2,3) & g = M * (3,1) & h = M * (3,2) & i = M * (3,3) )
ex s being FinSequence of K st
( s = M . 1 & M * (1,2) = s . 2 ) by A2, MATRIX_0:def 5;
hence M * (1,2) = b by A1, FINSEQ_1:45; :: thesis: ( c = M * (1,3) & d = M * (2,1) & e = M * (2,2) & f = M * (2,3) & g = M * (3,1) & h = M * (3,2) & i = M * (3,3) )
ex s being FinSequence of K st
( s = M . 1 & M * (1,3) = s . 3 ) by A2, MATRIX_0:def 5;
hence M * (1,3) = c by A1, FINSEQ_1:45; :: thesis: ( d = M * (2,1) & e = M * (2,2) & f = M * (2,3) & g = M * (3,1) & h = M * (3,2) & i = M * (3,3) )
ex s being FinSequence of K st
( s = M . 2 & M * (2,1) = s . 1 ) by A2, MATRIX_0:def 5;
hence M * (2,1) = d by A1, FINSEQ_1:45; :: thesis: ( e = M * (2,2) & f = M * (2,3) & g = M * (3,1) & h = M * (3,2) & i = M * (3,3) )
ex s being FinSequence of K st
( s = M . 2 & M * (2,2) = s . 2 ) by A2, MATRIX_0:def 5;
hence M * (2,2) = e by A1, FINSEQ_1:45; :: thesis: ( f = M * (2,3) & g = M * (3,1) & h = M * (3,2) & i = M * (3,3) )
ex s being FinSequence of K st
( s = M . 2 & M * (2,3) = s . 3 ) by A2, MATRIX_0:def 5;
hence M * (2,3) = f by A1, FINSEQ_1:45; :: thesis: ( g = M * (3,1) & h = M * (3,2) & i = M * (3,3) )
ex s being FinSequence of K st
( s = M . 3 & M * (3,1) = s . 1 ) by A2, MATRIX_0:def 5;
hence M * (3,1) = g by A1, FINSEQ_1:45; :: thesis: ( h = M * (3,2) & i = M * (3,3) )
ex s being FinSequence of K st
( s = M . 3 & M * (3,2) = s . 2 ) by A2, MATRIX_0:def 5;
hence M * (3,2) = h by A1, FINSEQ_1:45; :: thesis: i = M * (3,3)
ex s being FinSequence of K st
( s = M . 3 & M * (3,3) = s . 3 ) by A2, MATRIX_0:def 5;
hence M * (3,3) = i by A1, FINSEQ_1:45; :: thesis: verum