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