let x be set ; :: thesis: for n, k, m being Nat
for K being Field
for A being Matrix of the carrier of K,n,
for B being Matrix of the carrier of K,n, st n > 0 & x in Solutions_of A,B holds
x is Matrix of the carrier of K,k,
let n, k, m be Nat; :: thesis: for K being Field
for A being Matrix of the carrier of K,n,
for B being Matrix of the carrier of K,n, st n > 0 & x in Solutions_of A,B holds
x is Matrix of the carrier of K,k,
let K be Field; :: thesis: for A being Matrix of the carrier of K,n,
for B being Matrix of the carrier of K,n, st n > 0 & x in Solutions_of A,B holds
x is Matrix of the carrier of K,k,
let A be Matrix of the carrier of K,n,; :: thesis: for B being Matrix of the carrier of K,n, st n > 0 & x in Solutions_of A,B holds
x is Matrix of the carrier of K,k,
let B be Matrix of the carrier of K,n,; :: thesis: ( n > 0 & x in Solutions_of A,B implies x is Matrix of the carrier of K,k, )
assume n > 0 ; :: thesis: ( not x in Solutions_of A,B or x is Matrix of the carrier of K,k, )
then A1: ( width A = k & width B = m ) by MATRIX_1:24;
assume x in Solutions_of A,B ; :: thesis: x is Matrix of the carrier of K,k,
then ex X being Matrix of st
( X = x & len X = k & width X = m & A * X = B ) by A1;
hence x is Matrix of the carrier of K,k, by MATRIX_2:7; :: thesis: verum