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_0:24;

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 ) ; :: thesis: verum

( 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_0:24;

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 ) ; :: thesis: verum