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