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 (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 by MATRIX_1:25;
A4: width (1. K,n) = n by MATRIX_1:25;
then ( width (1. K,n) = 0 implies len (1. K,n) = 0 ) by MATRIX_1:25;
then x in Solutions_of (1. K,n),(n |-> (0. K)) by A2, A3, Def5;
then consider f being FinSequence of K such that
A5: f = x and
A6: ColVec2Mx f in Solutions_of (1. K,n),(ColVec2Mx (n |-> (0. K))) ;
consider X being Matrix of K such that
A7: X = ColVec2Mx f and
A8: len X = width (1. K,n) and
width X = width (ColVec2Mx (n |-> (0. K))) and
A9: (1. K,n) * X = ColVec2Mx (n |-> (0. K)) by A6;

A10: now

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

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

(1. K,n) * X = X by A4, A8, MATRIXR2:68;
hence n |-> (0. K) = Col X,1 by A9, A11, Th26
.= f by A4, A7, A8, A11, Th26 ;
:: thesis: verum

end;

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

then f = {} by A4, A7, A8, MATRIX_1:def 3;
hence f = n |-> (0. K) by A12; :: 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 A4, MATRIX13:102 ;
then f in {(0. (Space_of_Solutions_of (1. K,n)))} by A10, TARSKI:def 1;
hence x in the carrier of ((0). (Space_of_Solutions_of (1. K,n))) by A5, VECTSP_4:def 3; :: thesis: verum

end;

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;
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