for n being Element of NAT
for K being Field
for A being Matrix of n,K holds
( A = 1. (K,n) iff for i, j being Nat st 1 <= i & i <= n & 1 <= j & j <= n holds
A * (i,j) = IFEQ (i,j,(1. K),(0. K)) )