let V be RealLinearSpace; :: thesis: ( V is finite-dimensional iff (Omega). V is finite-dimensional )
set O = (Omega). V;
thus ( V is finite-dimensional implies (Omega). V is finite-dimensional ) ; :: thesis: ( (Omega). V is finite-dimensional implies V is finite-dimensional )
assume (Omega). V is finite-dimensional ; :: thesis: V is finite-dimensional
then consider A being finite Subset of ((Omega). V) such that
A1: A is Basis of (Omega). V by RLVECT_5:def 1;
A2: RLSStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #) = (Omega). V by RLSUB_1:def 4;
then reconsider a = A as finite Subset of V ;
Lin A = (Omega). V by A1, RLVECT_3:def 3;
then A3: Lin a = (Omega). V by RLVECT_5:20;
A is linearly-independent by A1, RLVECT_3:def 3;
then a is linearly-independent by RLVECT_5:14;
then a is Basis of V by A2, A3, RLVECT_3:def 3;
hence V is finite-dimensional by RLVECT_5:def 1; :: thesis: verum