let n be Nat; :: thesis: for K being Field holds dim (Space_of_Solutions_of (1. K,n)) = 0
let K be Field; :: thesis: dim (Space_of_Solutions_of (1. K,n)) = 0
set ONE = 1. K,n;
set SS = Space_of_Solutions_of (1. K,n);
A1: the carrier of ((0). (Space_of_Solutions_of (1. K,n))) c= the carrier of (Space_of_Solutions_of (1. K,n)) by VECTSP_4:def 2;
the carrier of (Space_of_Solutions_of (1. K,n)) c= the carrier of ((0). (Space_of_Solutions_of (1. K,n)))

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in the carrier of (Space_of_Solutions_of (1. K,n)) or x in the carrier of ((0). (Space_of_Solutions_of (1. K,n))) )
assume A2: x in the carrier of (Space_of_Solutions_of (1. K,n)) ; :: thesis: x in the carrier of ((0). (Space_of_Solutions_of (1. K,n)))
A3: ( len (1. K,n) = n & width (1. K,n) = n ) by MATRIX_1:25;
then ( width (1. K,n) = 0 implies len (1. K,n) = 0 ) ;
then x in Solutions_of (1. K,n),(n |-> (0. K)) by A2, Def5, A3;
then consider f being FinSequence of K such that
A4: ( f = x & ColVec2Mx f in Solutions_of (1. K,n),(ColVec2Mx (n |-> (0. K))) ) ;
consider X being Matrix of K such that
A5: ( X = ColVec2Mx f & len X = width (1. K,n) ) and
width X = width (ColVec2Mx (n |-> (0. K))) and
A6: (1. K,n) * X = ColVec2Mx (n |-> (0. K)) by A4;

A7: now

per cases ( n > 0 or n = 0 ) ;

suppose A8: n > 0 ; :: thesis: n |-> (0. K) = f

(1. K,n) * X = X by A3, A5, MATRIXR2:68;
hence n |-> (0. K) = Col X,1 by A6, A8, Th26
.= f by A3, A5, A8, Th26 ;
:: thesis: verum

end;

suppose n = 0 ; :: thesis: f = n |-> (0. K)

then ( len f = 0 & len (n |-> (0. K)) = 0 ) by A5, A3, MATRIX_1:def 3;
then ( f = {} & n |-> (0. K) = {} ) ;
hence f = n |-> (0. K) ; :: thesis: verum

end;

end;

end;

0. (Space_of_Solutions_of (1. K,n)) = 0. ((width (1. K,n)) -VectSp_over K) by VECTSP_4:19
.= n |-> (0. K) by A3, MATRIX13:102 ;
then f in {(0. (Space_of_Solutions_of (1. K,n)))} by A7, TARSKI:def 1;
hence x in the carrier of ((0). (Space_of_Solutions_of (1. K,n))) by A4, VECTSP_4:def 3; :: thesis: verum

end;

then the carrier of (Space_of_Solutions_of (1. K,n)) = the carrier of ((0). (Space_of_Solutions_of (1. K,n))) by A1, XBOOLE_0:def 10;
then (0). (Space_of_Solutions_of (1. K,n)) = (Omega). (Space_of_Solutions_of (1. K,n)) by VECTSP_4:37;
hence dim (Space_of_Solutions_of (1. K,n)) = 0 by VECTSP_9:33; :: thesis: verum