let n be Nat; :: thesis: for At being Subset of (TOP-REAL n)
for Ar being Subset of (REAL-NS n) st At = Ar holds
Lin At = Lin Ar
let At be Subset of (TOP-REAL n); :: thesis: for Ar being Subset of (REAL-NS n) st At = Ar holds
Lin At = Lin Ar
let Ar be Subset of (REAL-NS n); :: thesis: ( At = Ar implies Lin At = Lin Ar )
assume A1: At = Ar ; :: thesis: Lin At = Lin Ar
set V = TOP-REAL n;
set W = REAL-NS n;
set Lt = Lin At;
set Lr = Lin Ar;
A2: ( the carrier of (Lin At) c= the carrier of (TOP-REAL n) & 0. (Lin At) = 0. (TOP-REAL n) & the addF of (Lin At) = the addF of (TOP-REAL n) || the carrier of (Lin At) & the Mult of (Lin At) = the Mult of (TOP-REAL n) | [:REAL, the carrier of (Lin At):] ) by RLSUB_1:def 2;
A3: the carrier of (Lin At) = [#] (Lin At)
.= [#] (Lin Ar) by A1, Th26
.= the carrier of (Lin Ar) ;
A4: 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) #) = 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 Th1;
then ( the carrier of (TOP-REAL n) = the carrier of (REAL-NS n) & 0. (TOP-REAL n) = 0. (REAL-NS n) & the addF of (TOP-REAL n) = the addF of (REAL-NS n) & the Mult of (TOP-REAL n) = the Mult of (REAL-NS n) ) ;
then A5: 0. (Lin At) = 0. (Lin Ar) by A2, RLSUB_1:def 2;
A6: the addF of (Lin At) = the addF of (REAL-NS n) || the carrier of (Lin Ar) by A3, A4, RLSUB_1:def 2
.= the addF of (Lin Ar) by RLSUB_1:def 2 ;
the Mult of (Lin At) = the Mult of (REAL-NS n) | [:REAL, the carrier of (Lin Ar):] by A3, A4, RLSUB_1:def 2
.= the Mult of (Lin Ar) by RLSUB_1:def 2 ;
hence Lin At = Lin Ar by A3, A5, A6; :: thesis: verum