let m, n be Nat; :: thesis: for K being Field

for A being Matrix of 0 ,n,K

for B being Matrix of 0 ,m,K holds Solutions_of (A,B) = {{}}

let K be Field; :: thesis: for A being Matrix of 0 ,n,K

for B being Matrix of 0 ,m,K holds Solutions_of (A,B) = {{}}

let A be Matrix of 0 ,n,K; :: thesis: for B being Matrix of 0 ,m,K holds Solutions_of (A,B) = {{}}

let B be Matrix of 0 ,m,K; :: thesis: Solutions_of (A,B) = {{}}

A1: len A = 0 by MATRIX_0:def 2;

A2: Solutions_of (A,B) c= {{}}

then A3: ( B = {} & width B = 0 ) by MATRIX_0:def 3;

A4: width A = 0 by A1, MATRIX_0:def 3;

then len (A * A) = 0 by A1, MATRIX_3:def 4;

then A * A = {} ;

then A in Solutions_of (A,B) by A1, A4, A3;

hence Solutions_of (A,B) = {{}} by A2, ZFMISC_1:33; :: thesis: verum

for A being Matrix of 0 ,n,K

for B being Matrix of 0 ,m,K holds Solutions_of (A,B) = {{}}

let K be Field; :: thesis: for A being Matrix of 0 ,n,K

for B being Matrix of 0 ,m,K holds Solutions_of (A,B) = {{}}

let A be Matrix of 0 ,n,K; :: thesis: for B being Matrix of 0 ,m,K holds Solutions_of (A,B) = {{}}

let B be Matrix of 0 ,m,K; :: thesis: Solutions_of (A,B) = {{}}

A1: len A = 0 by MATRIX_0:def 2;

A2: Solutions_of (A,B) c= {{}}

proof

len B = 0
by MATRIX_0:def 2;
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in Solutions_of (A,B) or x in {{}} )

assume x in Solutions_of (A,B) ; :: thesis: x in {{}}

then ex X being Matrix of K st

( X = x & len X = width A & width X = width B & A * X = B ) ;

then x = {} by A1, MATRIX_0:def 3;

hence x in {{}} by TARSKI:def 1; :: thesis: verum

end;assume x in Solutions_of (A,B) ; :: thesis: x in {{}}

then ex X being Matrix of K st

( X = x & len X = width A & width X = width B & A * X = B ) ;

then x = {} by A1, MATRIX_0:def 3;

hence x in {{}} by TARSKI:def 1; :: thesis: verum

then A3: ( B = {} & width B = 0 ) by MATRIX_0:def 3;

A4: width A = 0 by A1, MATRIX_0:def 3;

then len (A * A) = 0 by A1, MATRIX_3:def 4;

then A * A = {} ;

then A in Solutions_of (A,B) by A1, A4, A3;

hence Solutions_of (A,B) = {{}} by A2, ZFMISC_1:33; :: thesis: verum