let n be Nat; for X being set holds
( X is Basis of TOP-REAL n iff X is Basis of REAL-NS n )
let X be set ; ( X is Basis of TOP-REAL n iff X is Basis of REAL-NS n )
set V = TOP-REAL n;
set W = REAL-NS n;
hereby ( X is Basis of REAL-NS n implies X is Basis of TOP-REAL n )
assume
X is
Basis of
TOP-REAL n
;
X is Basis of REAL-NS nthen reconsider A =
X as
Basis of
TOP-REAL n ;
reconsider B =
A as
Subset of
(REAL-NS n) by Th4;
A1:
(
A is
linearly-independent &
Lin A = RLSStruct(# the
carrier of
(TOP-REAL n), the
ZeroF of
(TOP-REAL n), the
addF of
(TOP-REAL n), the
Mult of
(TOP-REAL n) #) )
by RLVECT_3:def 3;
then A2:
B is
linearly-independent
by Th28;
set W0 =
(Omega). (REAL-NS n);
A3:
(Omega). (REAL-NS n) = RLSStruct(# the
carrier of
(REAL-NS n), the
ZeroF of
(REAL-NS n), the
addF of
(REAL-NS n), the
Mult of
(REAL-NS n) #)
by RLSUB_1:def 4;
A4:
Lin B is
strict Subspace of
(Omega). (REAL-NS n)
by Th49;
A5:
[#] (Lin A) = the
carrier of
(REAL-NS n)
by A1, Th4;
the
carrier of
(Lin B) =
[#] (Lin B)
.=
the
carrier of
((Omega). (REAL-NS n))
by A3, A5, Th26
;
then Lin B =
(Omega). (REAL-NS n)
by A4, RLSUB_1:32
.=
RLSStruct(# the
carrier of
(REAL-NS n), the
ZeroF of
(REAL-NS n), the
addF of
(REAL-NS n), the
Mult of
(REAL-NS n) #)
by RLSUB_1:def 4
;
hence
X is
Basis of
REAL-NS n
by A2, RLVECT_3:def 3;
verum
end;
assume
X is Basis of REAL-NS n
; X is Basis of TOP-REAL n
then reconsider A = X as Basis of REAL-NS n ;
reconsider B = A as Subset of (TOP-REAL n) by Th4;
A6:
( A is linearly-independent & Lin A = RLSStruct(# the carrier of (REAL-NS n), the ZeroF of (REAL-NS n), the addF of (REAL-NS n), the Mult of (REAL-NS n) #) )
by RLVECT_3:def 3;
then A7:
B is linearly-independent
by Th28;
set V0 = (Omega). (TOP-REAL n);
A8:
(Omega). (TOP-REAL n) = RLSStruct(# the carrier of (TOP-REAL n), the ZeroF of (TOP-REAL n), the addF of (TOP-REAL n), the Mult of (TOP-REAL n) #)
by RLSUB_1:def 4;
A9:
Lin B is strict Subspace of (Omega). (TOP-REAL n)
by Th49;
A10:
[#] (Lin A) = the carrier of (TOP-REAL n)
by A6, Th4;
the carrier of (Lin B) =
[#] (Lin B)
.=
the carrier of ((Omega). (TOP-REAL n))
by A8, A10, Th26
;
then Lin B =
(Omega). (TOP-REAL n)
by A9, RLSUB_1:32
.=
RLSStruct(# the carrier of (TOP-REAL n), the ZeroF of (TOP-REAL n), the addF of (TOP-REAL n), the Mult of (TOP-REAL n) #)
by RLSUB_1:def 4
;
hence
X is Basis of TOP-REAL n
by A7, RLVECT_3:def 3; verum