let V be finite-dimensional RealUnitarySpace; :: thesis: ( dim V = 0 iff (Omega). V = (0). V )

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

assume A1: dim V = 0 ; :: thesis: (Omega). V = (0). V
consider I being finite Subset of V such that
A2: I is Basis of V by Def1;
card I = 0 by A1, A2, Def3;
then A3: I = {} the carrier of V ;
(Omega). V = UNITSTR(# the carrier of V,the U2 of V,the addF of V,the Mult of V,the scalar of V #) by RUSUB_1:def 3
.= Lin I by A2, RUSUB_3:def 2
.= (0). V by A3, RUSUB_3:3 ;
hence (Omega). V = (0). V ; :: thesis: verum

end;

assume (Omega). V = (0). V ; :: thesis: dim V = 0
then A4: UNITSTR(# the carrier of V,the U2 of V,the addF of V,the Mult of V,the scalar of V #) = (0). V by RUSUB_1:def 3;
consider I being finite Subset of V such that
A5: I is Basis of V by Def1;
Lin I = (0). V by A4, A5, RUSUB_3:def 2;
then A6: ( I = {} or I = {(0. V)} ) by RUSUB_3:4;

now

assume I = {(0. V)} ; :: thesis: contradiction
then not I is linearly-independent by RLVECT_3:9;
hence contradiction by A5, RUSUB_3:def 2; :: thesis: verum

end;

hence dim V = 0 by A5, A6, Def3, CARD_1:47; :: thesis: verum