let n be Nat; :: thesis: for K being Field holds
( 1. (K,n) is Idempotent & 1. (K,n) is Involutory )
let K be Field; :: thesis: ( 1. (K,n) is Idempotent & 1. (K,n) is Involutory )
(1. (K,n)) * (1. (K,n)) = 1. (K,n) by MATRIX_3:20;
hence ( 1. (K,n) is Idempotent & 1. (K,n) is Involutory ) by Def1, Def3; :: thesis: verum