let n be Nat; :: thesis: for K being Field
for M1, M2 being Matrix of n,K st n > 0 & M1 is symmetric & M2 is symmetric holds
( M1 commutes_with M2 iff M1 * M2 is symmetric )
let K be Field; :: thesis: for M1, M2 being Matrix of n,K st n > 0 & M1 is symmetric & M2 is symmetric holds
( M1 commutes_with M2 iff M1 * M2 is symmetric )
let M1, M2 be Matrix of n,K; :: thesis: ( n > 0 & M1 is symmetric & M2 is symmetric implies ( M1 commutes_with M2 iff M1 * M2 is symmetric ) )
assume A1: ( n > 0 & M1 is symmetric & M2 is symmetric ) ; :: thesis: ( M1 commutes_with M2 iff M1 * M2 is symmetric )
then A2: ( M1 @ = M1 & M2 @ = M2 ) by Def5;
A3: ( M1 is Matrix of n,K & M2 is Matrix of n,K & width M1 = n & len M2 = n & width M2 = n & len M1 = n ) by MATRIX_1:25;
thus ( M1 commutes_with M2 implies M1 * M2 is symmetric ) :: thesis: ( M1 * M2 is symmetric implies M1 commutes_with M2 )

proof

assume A4: M1 commutes_with M2 ; :: thesis: M1 * M2 is symmetric
(M1 * M2) @ = M2 * M1 by A1, A2, A3, MATRIX_3:24
.= M1 * M2 by A4, Def1 ;
hence M1 * M2 is symmetric by Def5; :: thesis: verum

end;

assume A5: M1 * M2 is symmetric ; :: thesis: M1 commutes_with M2
M2 * M1 = (M1 * M2) @ by A1, A2, A3, MATRIX_3:24
.= M1 * M2 by A5, Def5 ;
hence M1 commutes_with M2 by Def1; :: thesis: verum