theorem :: MATRIX_6:35

for n being Nat
for K being Field
for M1, M2 being Matrix of n,K holds
( M1 commutes_with M2 iff (M1 + M2) * (M1 + M2) = (((M1 * M1) + (M1 * M2)) + (M1 * M2)) + (M2 * M2) )