let V be finite-dimensional RealLinearSpace; :: 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 Def1;

assume (Omega). V = (0). V ; :: thesis: dim V = 0

then RLSStruct(# the carrier of V, the ZeroF of V, the U5 of V, the Mult of V #) = (0). V by RLSUB_1:def 4;

then Lin I = (0). V by A1, RLVECT_3:def 3;

then ( I = {} or I = {(0. V)} ) by RLVECT_3:17;

hence dim V = 0 by A1, A4, Def2, CARD_1:27; :: thesis: verum

consider I being finite Subset of V such that

A1: I is Basis of V by Def1;

hereby :: thesis: ( (Omega). V = (0). V implies dim V = 0 )

A4:
I <> {(0. V)}
by A1, RLVECT_3:8, RLVECT_3:def 3;consider I being finite Subset of V such that

A2: I is Basis of V by Def1;

assume dim V = 0 ; :: thesis: (Omega). V = (0). V

then card I = 0 by A2, Def2;

then A3: I = {} the carrier of V ;

(Omega). V = RLSStruct(# the carrier of V, the ZeroF of V, the U5 of V, the Mult of V #) by RLSUB_1:def 4

.= Lin I by A2, RLVECT_3:def 3

.= (0). V by A3, RLVECT_3:16 ;

hence (Omega). V = (0). V ; :: thesis: verum

end;A2: I is Basis of V by Def1;

assume dim V = 0 ; :: thesis: (Omega). V = (0). V

then card I = 0 by A2, Def2;

then A3: I = {} the carrier of V ;

(Omega). V = RLSStruct(# the carrier of V, the ZeroF of V, the U5 of V, the Mult of V #) by RLSUB_1:def 4

.= Lin I by A2, RLVECT_3:def 3

.= (0). V by A3, RLVECT_3:16 ;

hence (Omega). V = (0). V ; :: thesis: verum

assume (Omega). V = (0). V ; :: thesis: dim V = 0

then RLSStruct(# the carrier of V, the ZeroF of V, the U5 of V, the Mult of V #) = (0). V by RLSUB_1:def 4;

then Lin I = (0). V by A1, RLVECT_3:def 3;

then ( I = {} or I = {(0. V)} ) by RLVECT_3:17;

hence dim V = 0 by A1, A4, Def2, CARD_1:27; :: thesis: verum