let x be set ; :: thesis: for k, m, n being Nat

for K being Field

for A being Matrix of n,k,K

for B being Matrix of n,m,K st n > 0 & x in Solutions_of (A,B) holds

x is Matrix of k,m,K

let k, m, n be Nat; :: thesis: for K being Field

for A being Matrix of n,k,K

for B being Matrix of n,m,K st n > 0 & x in Solutions_of (A,B) holds

x is Matrix of k,m,K

let K be Field; :: thesis: for A being Matrix of n,k,K

for B being Matrix of n,m,K st n > 0 & x in Solutions_of (A,B) holds

x is Matrix of k,m,K

let A be Matrix of n,k,K; :: thesis: for B being Matrix of n,m,K st n > 0 & x in Solutions_of (A,B) holds

x is Matrix of k,m,K

let B be Matrix of n,m,K; :: thesis: ( n > 0 & x in Solutions_of (A,B) implies x is Matrix of k,m,K )

assume n > 0 ; :: thesis: ( not x in Solutions_of (A,B) or x is Matrix of k,m,K )

then A1: ( width A = k & width B = m ) by MATRIX_0:23;

assume x in Solutions_of (A,B) ; :: thesis: x is Matrix of k,m,K

then ex X being Matrix of K st

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

hence x is Matrix of k,m,K by MATRIX_0:51; :: thesis: verum

for K being Field

for A being Matrix of n,k,K

for B being Matrix of n,m,K st n > 0 & x in Solutions_of (A,B) holds

x is Matrix of k,m,K

let k, m, n be Nat; :: thesis: for K being Field

for A being Matrix of n,k,K

for B being Matrix of n,m,K st n > 0 & x in Solutions_of (A,B) holds

x is Matrix of k,m,K

let K be Field; :: thesis: for A being Matrix of n,k,K

for B being Matrix of n,m,K st n > 0 & x in Solutions_of (A,B) holds

x is Matrix of k,m,K

let A be Matrix of n,k,K; :: thesis: for B being Matrix of n,m,K st n > 0 & x in Solutions_of (A,B) holds

x is Matrix of k,m,K

let B be Matrix of n,m,K; :: thesis: ( n > 0 & x in Solutions_of (A,B) implies x is Matrix of k,m,K )

assume n > 0 ; :: thesis: ( not x in Solutions_of (A,B) or x is Matrix of k,m,K )

then A1: ( width A = k & width B = m ) by MATRIX_0:23;

assume x in Solutions_of (A,B) ; :: thesis: x is Matrix of k,m,K

then ex X being Matrix of K st

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

hence x is Matrix of k,m,K by MATRIX_0:51; :: thesis: verum