theorem :: MATRIX_6:30

for K being Fanoian Field
for n, i being Nat
for M1 being Matrix of n,K st M1 is antisymmetric & i in Seg n holds
M1 * (i,i) = 0. K