theorem :: MATRIX_8:3

for n being Nat
for K being Field
for M1 being Matrix of n,K st n > 0 holds
( M1 is Idempotent iff M1 @ is Idempotent )