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 object ; :: 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_0:24;
A4: width (1. (K,n)) = n by MATRIX_0:24;
then ( width (1. (K,n)) = 0 implies len (1. (K,n)) = 0 ) by MATRIX_0:24;
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 :: thesis: n |-> (0. K) = f

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_0:def 2;
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:11
.= 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;
then (0). (Space_of_Solutions_of (1. (K,n))) = (Omega). (Space_of_Solutions_of (1. (K,n))) by VECTSP_4:29;
hence dim (Space_of_Solutions_of (1. (K,n))) = 0 by VECTSP_9:29; :: thesis: verum