let n, m 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_1:def 3;
A2: Solutions_of A,B c= {{} }

proof

let x be set ; :: 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_1:def 4;
hence x in {{} } by TARSKI:def 1; :: thesis: verum

end;

len B = 0 by MATRIX_1:def 3;
then A3: ( B = {} & width B = 0 ) by MATRIX_1:def 4;
A4: width A = 0 by A1, MATRIX_1:def 4;
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:39; :: thesis: verum