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 & len B = 0 ) by MATRIX_1:def 3;
then A2: ( width A = 0 & B = {} & width B = 0 ) by MATRIX_1:def 4;
A3: 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 A4: x in Solutions_of A,B ; :: thesis: x in {{} }
ex X being Matrix of K st
( X = x & len X = width A & width X = width B & A * X = B ) by A4;
then x = {} by A2;
hence x in {{} } by TARSKI:def 1; :: thesis: verum

end;

len (A * A) = 0 by A1, A2, MATRIX_3:def 4;
then A * A = {} ;
then A in Solutions_of A,B by A1, A2;
hence Solutions_of A,B = {{} } by A3, ZFMISC_1:39; :: thesis: verum