let k, m, n 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_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 } :: 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)))

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_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; :: thesis: verum

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_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 } :: 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 object ; :: 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))) )
let x be object ; :: 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;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

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_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; :: thesis: verum