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

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

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

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

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

0. (Space_of_Solutions_of (1. (K,n))) =
0. ((width (1. (K,n))) -VectSp_over K)
by VECTSP_4:11
end;

.= 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

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