let GF be Field; :: thesis: for V being finite-dimensional VectSp of GF holds
( dim V = 0 iff (Omega). V = (0). V )
let V be finite-dimensional VectSp of GF; :: thesis: ( dim V = 0 iff (Omega). V = (0). V )
consider I being finite Subset of V such that
A1: I is Basis of V by MATRLIN:def 1;
hereby :: thesis: ( (Omega). V = (0). V implies dim V = 0 )
consider I being finite Subset of V such that
A2: I is Basis of V by MATRLIN:def 1;
assume dim V = 0 ; :: thesis: (Omega). V = (0). V
then card I = 0 by A2, Def1;
then A3: I = {} the carrier of V ;
(Omega). V = ModuleStr(# the carrier of V, the U5 of V, the ZeroF of V, the lmult of V #) by VECTSP_4:def 4
.= Lin I by A2, VECTSP_7:def 3
.= (0). V by A3, VECTSP_7:9 ;
hence (Omega). V = (0). V ; :: thesis: verum
end;
A4: I <> {(0. V)} by A1, VECTSP_7:3, VECTSP_7:def 3;
assume (Omega). V = (0). V ; :: thesis: dim V = 0
then ModuleStr(# the carrier of V, the U5 of V, the ZeroF of V, the lmult of V #) = (0). V by VECTSP_4:def 4;
then Lin I = (0). V by A1, VECTSP_7:def 3;
then ( I = {} or I = {(0. V)} ) by VECTSP_7:10;
hence dim V = 0 by A1, A4, Def1, CARD_1:27; :: thesis: verum