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