let K be Field; :: thesis: for M being Matrix of 3,K ex a, b, c, d, e, f, g, h, i being Element of K st M = <*<*a,b,c*>,<*d,e,f*>,<*g,h,i*>*>
let M be Matrix of 3,K; :: thesis: ex a, b, c, d, e, f, g, h, i being Element of K st M = <*<*a,b,c*>,<*d,e,f*>,<*g,h,i*>*>
reconsider 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) as Element of K ;
take a ; :: thesis: ex b, c, d, e, f, g, h, i being Element of K st M = <*<*a,b,c*>,<*d,e,f*>,<*g,h,i*>*>
take b ; :: thesis: ex c, d, e, f, g, h, i being Element of K st M = <*<*a,b,c*>,<*d,e,f*>,<*g,h,i*>*>
take c ; :: thesis: ex d, e, f, g, h, i being Element of K st M = <*<*a,b,c*>,<*d,e,f*>,<*g,h,i*>*>
take d ; :: thesis: ex e, f, g, h, i being Element of K st M = <*<*a,b,c*>,<*d,e,f*>,<*g,h,i*>*>
take e ; :: thesis: ex f, g, h, i being Element of K st M = <*<*a,b,c*>,<*d,e,f*>,<*g,h,i*>*>
take f ; :: thesis: ex g, h, i being Element of K st M = <*<*a,b,c*>,<*d,e,f*>,<*g,h,i*>*>
take g ; :: thesis: ex h, i being Element of K st M = <*<*a,b,c*>,<*d,e,f*>,<*g,h,i*>*>
take h ; :: thesis: ex i being Element of K st M = <*<*a,b,c*>,<*d,e,f*>,<*g,h,i*>*>
take i ; :: thesis: M = <*<*a,b,c*>,<*d,e,f*>,<*g,h,i*>*>
thus M = <*<*a,b,c*>,<*d,e,f*>,<*g,h,i*>*> by MATRIXR2:37; :: thesis: verum