for n being Nat
for K being Field holds
( 1. (K,n) is Idempotent & 1. (K,n) is Involutory ) by MATRIX_3:18;