let n be Nat; :: thesis: for K being Field holds
( 0. K,n is Idempotent & 0. K,n is Nilpotent )
let K be Field; :: thesis: ( 0. K,n is Idempotent & 0. K,n is Nilpotent )
( width (0. K,n,n) = n & len (0. K,n,n) = n & width (0. K,n) = n & len (0. K,n) = n ) by MATRIX_1:25;
then (0. K,n,n) * (0. K,n) = 0. K,n,n by MATRIX_6:1;
hence ( 0. K,n is Idempotent & 0. K,n is Nilpotent ) by Def1, Def2; :: thesis: verum