let RNS0 be RealNormSpace; :: thesis:
reconsider RNS = NORMSTR(# the carrier of RNS0, the ZeroF of RNS0, the addF of RNS0, the Mult of RNS0, the normF of RNS0 #) as strict RealNormSpace by Th22;
set LRNS = LinearTopSpaceNorm RNS;
A1: ( the carrier of (LinearTopSpaceNorm RNS) = the carrier of RNS & 0. (LinearTopSpaceNorm RNS) = 0. RNS & the addF of (LinearTopSpaceNorm RNS) = the addF of RNS & the Mult of (LinearTopSpaceNorm RNS) = the Mult of RNS & the topology of (LinearTopSpaceNorm RNS) = the topology of (TopSpaceNorm RNS) ) by NORMSP_2:def 4;
reconsider N = the normF of RNS as Function of the carrier of (LinearTopSpaceNorm RNS),REAL by A1;
set W = RLNormTopStruct(# the carrier of (LinearTopSpaceNorm RNS), the ZeroF of (LinearTopSpaceNorm RNS), the addF of (LinearTopSpaceNorm RNS), the Mult of (LinearTopSpaceNorm RNS), the topology of (LinearTopSpaceNorm RNS),N #);

now :: thesis:

end;

proof

proof

let x1, x2 be Point of RLNormTopStruct(# the carrier of (LinearTopSpaceNorm RNS), the ZeroF of (LinearTopSpaceNorm RNS), the addF of (LinearTopSpaceNorm RNS), the Mult of (LinearTopSpaceNorm RNS), the topology of (LinearTopSpaceNorm RNS),N #); :: thesis:
let V be Subset of RLNormTopStruct(# the carrier of (LinearTopSpaceNorm RNS), the ZeroF of (LinearTopSpaceNorm RNS), the addF of (LinearTopSpaceNorm RNS), the Mult of (LinearTopSpaceNorm RNS), the topology of (LinearTopSpaceNorm RNS),N #); :: thesis:
assume A5: ( V is open & x1 + x2 in V ) ; :: thesis:
reconsider V0 = V as Subset of (LinearTopSpaceNorm RNS) ;
reconsider xx1 = x1, xx2 = x2 as Point of (LinearTopSpaceNorm RNS) ;
( V0 is open & xx1 + xx2 in V0 ) by A5;
then consider V10, V20 being Subset of (LinearTopSpaceNorm RNS) such that
A6: ( V10 is open & V20 is open & xx1 in V10 & xx2 in V20 & V10 + V20 c= V0 ) by RLTOPSP1:def 8;
reconsider V1 = V10, V2 = V20 as Subset of RLNormTopStruct(# the carrier of (LinearTopSpaceNorm RNS), the ZeroF of (LinearTopSpaceNorm RNS), the addF of (LinearTopSpaceNorm RNS), the Mult of (LinearTopSpaceNorm RNS), the topology of (LinearTopSpaceNorm RNS),N #) ;
A7: for z being object holds
( z in V10 + V20 iff z in V1 + V2 )

proof

let z be object ; :: thesis:

hereby :: thesis:

assume z in V10 + V20 ; :: thesis:
then consider u0, v0 being Element of (LinearTopSpaceNorm RNS) such that
A8: ( z = u0 + v0 & u0 in V10 & v0 in V20 ) ;
reconsider u = u0, v = v0 as Element of RLNormTopStruct(# the carrier of (LinearTopSpaceNorm RNS), the ZeroF of (LinearTopSpaceNorm RNS), the addF of (LinearTopSpaceNorm RNS), the Mult of (LinearTopSpaceNorm RNS), the topology of (LinearTopSpaceNorm RNS),N #) ;
u + v = u0 + v0 ;
hence z in V1 + V2 by A8; :: thesis:

end;

assume z in V1 + V2 ; :: thesis:
then consider u0, v0 being Element of RLNormTopStruct(# the carrier of (LinearTopSpaceNorm RNS), the ZeroF of (LinearTopSpaceNorm RNS), the addF of (LinearTopSpaceNorm RNS), the Mult of (LinearTopSpaceNorm RNS), the topology of (LinearTopSpaceNorm RNS),N #) such that
A9: ( z = u0 + v0 & u0 in V10 & v0 in V20 ) ;
reconsider u = u0, v = v0 as Element of (LinearTopSpaceNorm RNS) ;
u + v = u0 + v0 ;
hence z in V10 + V20 by A9; :: thesis:

end;

take V1 ; :: thesis:
take V2 ; :: thesis:
thus ( V1 is open & V2 is open & x1 in V1 & x2 in V2 & V1 + V2 c= V ) by A6, A7; :: thesis:

end;

A10: now :: thesis:

let a, b be Real; :: thesis:
let v be VECTOR of RLNormTopStruct(# the carrier of (LinearTopSpaceNorm RNS), the ZeroF of (LinearTopSpaceNorm RNS), the addF of (LinearTopSpaceNorm RNS), the Mult of (LinearTopSpaceNorm RNS), the topology of (LinearTopSpaceNorm RNS),N #); :: thesis:
reconsider v1 = v as VECTOR of (LinearTopSpaceNorm RNS) ;
A11: (a * v1) + (b * v1) = (a * v) + (b * v) ;
(a + b) * v = (a + b) * v1 ;
hence (a + b) * v = (a * v) + (b * v) by A11, RLVECT_1:def 6; :: thesis:

end;

proof

proof

let s be Real; :: thesis:
assume |.(s - a).| < r ; :: thesis:
then A15: s * Z0 c= V0 by A14;
for z being object holds
( z in s * Z0 iff z in s * Z )

proof

let z be object ; :: thesis:

hereby :: thesis:

assume z in s * Z0 ; :: thesis:
then consider u0 being Element of (LinearTopSpaceNorm RNS) such that
A16: ( z = s * u0 & u0 in Z0 ) ;
reconsider u = u0 as Element of RLNormTopStruct(# the carrier of (LinearTopSpaceNorm RNS), the ZeroF of (LinearTopSpaceNorm RNS), the addF of (LinearTopSpaceNorm RNS), the Mult of (LinearTopSpaceNorm RNS), the topology of (LinearTopSpaceNorm RNS),N #) ;
s * u = s * u0 ;
hence z in s * Z by A16; :: thesis:

end;

assume z in s * Z ; :: thesis:
then consider u0 being Element of RLNormTopStruct(# the carrier of (LinearTopSpaceNorm RNS), the ZeroF of (LinearTopSpaceNorm RNS), the addF of (LinearTopSpaceNorm RNS), the Mult of (LinearTopSpaceNorm RNS), the topology of (LinearTopSpaceNorm RNS),N #) such that
A17: ( z = s * u0 & u0 in Z0 ) ;
reconsider u = u0 as Element of (LinearTopSpaceNorm RNS) ;
s * u = s * u0 ;
hence z in s * Z0 by A17; :: thesis:

end;

hence s * Z c= V by A15; :: thesis:

end;

hence ( Z is open & x in Z & ( for s being Real st |.(s - a).| < r holds
s * Z c= V ) ) by A14; :: thesis:

end;

A18: RLNormTopStruct(# the carrier of (LinearTopSpaceNorm RNS), the ZeroF of (LinearTopSpaceNorm RNS), the addF of (LinearTopSpaceNorm RNS), the Mult of (LinearTopSpaceNorm RNS), the topology of (LinearTopSpaceNorm RNS),N #) is Abelian

proof

let v, w be VECTOR of RLNormTopStruct(# the carrier of (LinearTopSpaceNorm RNS), the ZeroF of (LinearTopSpaceNorm RNS), the addF of (LinearTopSpaceNorm RNS), the Mult of (LinearTopSpaceNorm RNS), the topology of (LinearTopSpaceNorm RNS),N #); :: according to RLVECT_1:def 2 :: thesis:
reconsider v1 = v, w1 = w as VECTOR of (LinearTopSpaceNorm RNS) ;
thus v + w = v1 + w1
.= w1 + v1
.= w + v ; :: thesis:

end;

A19: RLNormTopStruct(# the carrier of (LinearTopSpaceNorm RNS), the ZeroF of (LinearTopSpaceNorm RNS), the addF of (LinearTopSpaceNorm RNS), the Mult of (LinearTopSpaceNorm RNS), the topology of (LinearTopSpaceNorm RNS),N #) is add-associative

proof

let v, w, x be VECTOR of RLNormTopStruct(# the carrier of (LinearTopSpaceNorm RNS), the ZeroF of (LinearTopSpaceNorm RNS), the addF of (LinearTopSpaceNorm RNS), the Mult of (LinearTopSpaceNorm RNS), the topology of (LinearTopSpaceNorm RNS),N #); :: according to RLVECT_1:def 3 :: thesis:
reconsider v1 = v, w1 = w, x1 = x as VECTOR of (LinearTopSpaceNorm RNS) ;
thus (v + w) + x = (v1 + w1) + x1
.= v1 + (w1 + x1) by RLVECT_1:def 3
.= v + (w + x) ; :: thesis:

end;

A20: RLNormTopStruct(# the carrier of (LinearTopSpaceNorm RNS), the ZeroF of (LinearTopSpaceNorm RNS), the addF of (LinearTopSpaceNorm RNS), the Mult of (LinearTopSpaceNorm RNS), the topology of (LinearTopSpaceNorm RNS),N #) is right_zeroed

proof

end;

A21: RLNormTopStruct(# the carrier of (LinearTopSpaceNorm RNS), the ZeroF of (LinearTopSpaceNorm RNS), the addF of (LinearTopSpaceNorm RNS), the Mult of (LinearTopSpaceNorm RNS), the topology of (LinearTopSpaceNorm RNS),N #) is right_complementable

proof

end;

A22: now :: thesis:

let a, b be Real; :: thesis:
let v be VECTOR of RLNormTopStruct(# the carrier of (LinearTopSpaceNorm RNS), the ZeroF of (LinearTopSpaceNorm RNS), the addF of (LinearTopSpaceNorm RNS), the Mult of (LinearTopSpaceNorm RNS), the topology of (LinearTopSpaceNorm RNS),N #); :: thesis:
reconsider v1 = v as VECTOR of (LinearTopSpaceNorm RNS) ;
a * (b * v1) = a * (b * v) ;
then (a * b) * v1 = a * (b * v) by RLVECT_1:def 7;
hence (a * b) * v = a * (b * v) ; :: thesis:

end;

A23: now :: thesis:

let a be Real; :: thesis:
let v, w be VECTOR of RLNormTopStruct(# the carrier of (LinearTopSpaceNorm RNS), the ZeroF of (LinearTopSpaceNorm RNS), the addF of (LinearTopSpaceNorm RNS), the Mult of (LinearTopSpaceNorm RNS), the topology of (LinearTopSpaceNorm RNS),N #); :: thesis:
reconsider v1 = v, w1 = w as VECTOR of (LinearTopSpaceNorm RNS) ;
A24: (a * v1) + (a * w1) = (a * v) + (a * w) ;
a * (v + w) = a * (v1 + w1) ;
hence a * (v + w) = (a * v) + (a * w) by A24, RLVECT_1:def 5; :: thesis:

end;

now :: thesis:

end;

end;

now :: thesis:

end;