let K be Field; :: thesis: for n being Nat
for M1, M2 being Matrix of n,K st M2 is_reverse_of M1 holds
M1 commutes_with M2
let n be Nat; :: thesis: for M1, M2 being Matrix of n,K st M2 is_reverse_of M1 holds
M1 commutes_with M2
let M1, M2 be Matrix of n,K; :: thesis: ( M2 is_reverse_of M1 implies M1 commutes_with M2 )
assume M2 is_reverse_of M1 ; :: thesis: M1 commutes_with M2
then M2 * M1 = M1 * M2 by Def2;
hence M1 commutes_with M2 by Def1; :: thesis: verum