theorem Th1: :: MATRIX_8:1

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