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

proof

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;

len B = 0 by MATRIX_0:def 2;
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