let k, m, n be Nat; 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; ( 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
; 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_0:23;
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 }
XBOOLE_0:def 10 { 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
object ;
TARSKI:def 3 ( 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)))
;
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 }
;
verum
end;
let x be object ; TARSKI:def 3 ( 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 }
; 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_0:23;
A6:
width X = m
by A2, MATRIX_0:23;
len (0. (K,n,k)) = n
by A1, MATRIX_0:23;
then
(0. (K,n,k)) * X = 0. (K,n,m)
by A1, A2, A5, A6, MATRIX_5:22;
hence
x in Solutions_of ((0. (K,n,k)),(0. (K,n,m)))
by A4, A3, A5, A6; verum