let K be Field; :: thesis: for A, B being Matrix of K st not Solutions_of (A,B) is empty holds

len A = len B

let A, B be Matrix of K; :: thesis: ( not Solutions_of (A,B) is empty implies len A = len B )

assume not Solutions_of (A,B) is empty ; :: thesis: len A = len B

then consider x being object such that

A1: x in Solutions_of (A,B) ;

ex X being Matrix of K st

( X = x & len X = width A & width X = width B & A * X = B ) by A1;

hence len A = len B by MATRIX_3:def 4; :: thesis: verum

len A = len B

let A, B be Matrix of K; :: thesis: ( not Solutions_of (A,B) is empty implies len A = len B )

assume not Solutions_of (A,B) is empty ; :: thesis: len A = len B

then consider x being object such that

A1: x in Solutions_of (A,B) ;

ex X being Matrix of K st

( X = x & len X = width A & width X = width B & A * X = B ) by A1;

hence len A = len B by MATRIX_3:def 4; :: thesis: verum