let n be Nat; for K being Field holds Solutions_of ((0. (K,n,0)),(0. (K,n,0))) = {{}}
let K be Field; Solutions_of ((0. (K,n,0)),(0. (K,n,0))) = {{}}
per cases
( n = 0 or n > 0 )
;
suppose A1:
n > 0
;
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 ;
TARSKI:def 3 ( 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)))
;
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;
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;
verum end;