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_1:13;
A2: width (0. K,n,0 ) = 0 by A1, MATRIX_1:24;
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:113;
A4: 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;

A5: len E = 0 ;
A6: width E = 0 by MATRIX_1:25;
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_1:24;
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_1: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:39; :: thesis: verum

end;

end;