let n, k, m be Nat; :: thesis: for K being Field st n > 0 & k > 0 holds
Solutions_of (0. K,n,k),(0. K,n,m) = { X where X is Matrix of k,m,K : verum }
let K be Field; :: thesis: ( n > 0 & k > 0 implies Solutions_of (0. K,n,k),(0. K,n,m) = { X where X is Matrix of k,m,K : verum } )
assume that
A1: n > 0 and
A2: k > 0 ; :: thesis: Solutions_of (0. K,n,k),(0. K,n,m) = { X where X is Matrix of k,m,K : verum }
set B = 0. K,n,m;
A3: width (0. K,n,m) = m by A1, MATRIX_1:24;
set XX = { X where X is Matrix of k,m,K : verum } ;
set A = 0. K,n,k;
thus Solutions_of (0. K,n,k),(0. K,n,m) c= { X where X is Matrix of k,m,K : verum } :: according to XBOOLE_0:def 10 :: thesis: { X where X is Matrix of k,m,K : verum } c= Solutions_of (0. K,n,k),(0. K,n,m)

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in Solutions_of (0. K,n,k),(0. K,n,m) or x in { X where X is Matrix of k,m,K : verum } )
assume x in Solutions_of (0. K,n,k),(0. K,n,m) ; :: thesis: x in { X where X is Matrix of k,m,K : verum }
then x is Matrix of k,m,K by A1, Th53;
hence x in { X where X is Matrix of k,m,K : verum } ; :: thesis: verum

end;

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in { X where X is Matrix of k,m,K : verum } or x in Solutions_of (0. K,n,k),(0. K,n,m) )
assume x in { X where X is Matrix of k,m,K : verum } ; :: thesis: x in Solutions_of (0. K,n,k),(0. K,n,m)
then consider X being Matrix of k,m,K such that
A4: x = X and
verum ;
A5: ( width (0. K,n,k) = k & len X = k ) by A1, A2, MATRIX_1:24;
A6: width X = m by A2, MATRIX_1:24;
len (0. K,n,k) = n by A1, MATRIX_1:24;
then (0. K,n,k) * X = 0. K,n,m by A1, A2, A5, A6, MATRIX_5:38;
hence x in Solutions_of (0. K,n,k),(0. K,n,m) by A4, A3, A5, A6; :: thesis: verum