theorem Th54: :: MATRIX15:54

for k, m, n being Nat
for K being Field st n > 0 & k > 0 holds
Solutions_of ((0. (K,n,k)),(0. (K,n,m))) = { X where X is Matrix of k,m,K : verum }