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*>*> & M is symmetric holds
( b = d & c = g & h = f )
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*>*> & M is symmetric holds
( b = d & c = g & h = f )
let M be Matrix of 3,K; :: thesis: ( M = <*<*a,b,c*>,<*d,e,f*>,<*g,h,i*>*> & M is symmetric implies ( b = d & c = g & h = f ) )
assume that
A1: M = <*<*a,b,c*>,<*d,e,f*>,<*g,h,i*>*> and
A2: M is symmetric ; :: thesis: ( b = d & c = g & h = f )
A3: M = M @ by A2, MATRIX_6:def 5;
M @ = <*<*a,d,g*>,<*b,e,h*>,<*c,f,i*>*> by A1, Th05;
hence ( b = d & c = g & h = f ) by A1, A3, Th02; :: thesis: verum