let K be Field; 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; 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; ( 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
; ( 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; verum