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 A1:
( n > 0 & k > 0 )
; :: thesis: Solutions_of (0. K,n,k),(0. K,n,m) = { X where X is Matrix of k,m,K : verum }
set A = 0. K,n,k;
set B = 0. K,n,m;
set XX = { X where X is Matrix of k,m,K : verum } ;
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 A2:
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)
consider X being Matrix of k,m,K such that
A3:
x = X
by A2;
A4:
( len (0. K,n,k) = n & width (0. K,n,k) = k & len (0. K,n,m) = n & width (0. K,n,m) = m & len X = k & width X = m )
by A1, MATRIX_1:24;
then
(0. K,n,k) * X = 0. K,n,m
by A1, MATRIX_5:38;
hence
x in Solutions_of (0. K,n,k),(0. K,n,m)
by A3, A4; :: thesis: verum