let x be set ; :: thesis: for n, k, m 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 n, k, m 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 A1: n > 0 ; :: thesis: ( not x in Solutions_of A,B or x is Matrix of k,m,K )
A2: ( width A = k & width B = m ) by A1, MATRIX_1:24;
assume x in Solutions_of A,B ; :: thesis: x is Matrix of k,m,K
then consider X being Matrix of K such that
A3: ( X = x & len X = k & width X = m & A * X = B ) by A2;
thus x is Matrix of k,m,K by A3, MATRIX_2:7; :: thesis: verum