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