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

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

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

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

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;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

A5:
len E = 0
;
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;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

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