let n be Nat; :: thesis: for K being Field holds Solutions_of ((0. (K,n,0)),(0. (K,n,0))) = {{}}
let K be Field; :: thesis: Solutions_of ((0. (K,n,0)),(0. (K,n,0))) = {{}}

per cases ( n = 0 or n > 0 ) ;

suppose n = 0 ; :: thesis: Solutions_of ((0. (K,n,0)),(0. (K,n,0))) = {{}}

hence Solutions_of ((0. (K,n,0)),(0. (K,n,0))) = {{}} by Th51; :: thesis: verum

end;

suppose A1: n > 0 ; :: thesis: Solutions_of ((0. (K,n,0)),(0. (K,n,0))) = {{}}

set B = 0. (K,n,0);
set A = 0. (K,n,0);
reconsider E = {} as Matrix of 0 , 0 ,K by MATRIX_0:13;
A2: width (0. (K,n,0)) = 0 by A1, MATRIX_0:23;
then A3: for i, j being Nat st [i,j] in Indices (0. (K,n,0)) holds
(0. (K,n,0)) * (i,j) = ((0. (K,n,0)) * E) * (i,j) by ZFMISC_1:90;
A4: Solutions_of ((0. (K,n,0)),(0. (K,n,0))) c= {{}}

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in Solutions_of ((0. (K,n,0)),(0. (K,n,0))) or x in {{}} )
assume x in Solutions_of ((0. (K,n,0)),(0. (K,n,0))) ; :: thesis: x in {{}}
then reconsider X = x as Matrix of 0 , 0 ,K by A1, Th53;
len X = 0 by MATRIX_0:def 2;
then X = {} ;
hence x in {{}} by TARSKI:def 1; :: thesis: verum

end;

A5: len E = 0 ;
A6: width E = 0 by MATRIX_0:24;
then A7: width ((0. (K,n,0)) * E) = 0 by A2, A5, MATRIX_3:def 4;
A8: len (0. (K,n,0)) = n by A1, MATRIX_0:23;
then len ((0. (K,n,0)) * E) = n by A2, A5, MATRIX_3:def 4;
then (0. (K,n,0)) * E = 0. (K,n,0) by A8, A2, A7, A3, MATRIX_0:21;
then E in Solutions_of ((0. (K,n,0)),(0. (K,n,0))) by A2, A5, A6;
hence Solutions_of ((0. (K,n,0)),(0. (K,n,0))) = {{}} by A4, ZFMISC_1:33; :: thesis: verum

end;

end;