theorem Th56: :: MATRIX15:56

for n being Nat
for K being Field holds Solutions_of ((0. (K,n,0)),(0. (K,n,0))) = {{}}