let m, n be Nat; 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; 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; for B being Matrix of 0 ,m,K holds Solutions_of (A,B) = {{}}
let B be Matrix of 0 ,m,K; Solutions_of (A,B) = {{}}
A1:
len A = 0
by MATRIX_0:def 2;
A2:
Solutions_of (A,B) c= {{}}
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; verum