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

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