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 ) 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