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 ) = {{} }

reconsider E = {} as Matrix of 0 , 0 ,K by MATRIX_1:13;
set A = 0. K,n,0 ;
set B = 0. K,n,0 ;
A2: ( len (0. K,n,0 ) = n & width (0. K,n,0 ) = 0 & len (0. K,n,0 ) = n & width (0. K,n,0 ) = 0 & len E = 0 & width E = 0 & Indices (0. K,n,0 ) = [:(Seg n),(Seg 0 ):] ) by A1, MATRIX_1:24, MATRIX_1:25;
then A3: ( len ((0. K,n,0 ) * E) = n & width ((0. K,n,0 ) * E) = 0 ) by MATRIX_3:def 4;
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 A2, ZFMISC_1:113;
then (0. K,n,0 ) * E = 0. K,n,0 by A2, A3, MATRIX_1:21;
then A4: E in Solutions_of (0. K,n,0 ),(0. K,n,0 ) by A2;
Solutions_of (0. K,n,0 ),(0. K,n,0 ) c= {{} }

proof

let x be set ; :: 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_1:def 3;
then X = {} ;
hence x in {{} } by TARSKI:def 1; :: thesis: verum

end;

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

end;

end;