thus LinearTopSpaceNorm X is add-continuous :: thesis:

proof

let x1, x2 be Point of (LinearTopSpaceNorm X); :: according to RLTOPSP1:def 8 :: thesis:
let V be Subset of (LinearTopSpaceNorm X); :: thesis:
assume A1: ( V is open & x1 + x2 in V ) ; :: thesis:
reconsider z12 = x1 + x2 as Element of (MetricSpaceNorm X) by Def4;
reconsider z1 = x1 as Element of (MetricSpaceNorm X) by Def4;
reconsider z2 = x2 as Element of (MetricSpaceNorm X) by Def4;
V in the topology of (LinearTopSpaceNorm X) by A1, PRE_TOPC:def 5;
then V in the topology of (TopSpaceNorm X) by Def4;
then consider r being Real such that
A2: ( r > 0 & Ball z12,r c= V ) by A1, PCOMPS_1:def 5;
reconsider V1 = Ball z1,(r / 2), V2 = Ball z2,(r / 2) as Subset of (LinearTopSpaceNorm X) by Def4;
( Ball z1,(r / 2) in the topology of (TopSpaceNorm X) & Ball z2,(r / 2) in the topology of (TopSpaceNorm X) ) by PCOMPS_1:33;
then ( Ball z1,(r / 2) in the topology of (LinearTopSpaceNorm X) & Ball z2,(r / 2) in the topology of (LinearTopSpaceNorm X) ) by Def4;
then A3: ( V1 is open & V2 is open ) by PRE_TOPC:def 5;
set r2 = r / 2;
A4: 0 < r / 2 by A2, XREAL_1:217;
( dist z1,z1 = 0 & dist z2,z2 = 0 ) by METRIC_1:1;
then A5: ( x1 in V1 & x2 in V2 ) by A4, METRIC_1:12;
V1 + V2 c= V

proof

let w be set ; :: according to TARSKI:def 3 :: thesis:
assume w in V1 + V2 ; :: thesis:
then consider v, u being VECTOR of (LinearTopSpaceNorm X) such that
A6: ( w = v + u & v in V1 & u in V2 ) ;
reconsider v1 = v, u1 = u as Element of (MetricSpaceNorm X) by Def4;
reconsider w1 = w as Element of (MetricSpaceNorm X) by A6, Def4;
reconsider zz12 = x1 + x2, zz1 = x1, zz2 = x2, vv1 = v, uu1 = u as Point of X by Def4;
reconsider ww1 = w as Point of X by A6, Def4;
A7: dist z12,w1 = ||.(zz12 - ww1).|| by Def1
.= ||.((zz1 + zz2) - ww1).|| by Def4
.= ||.((zz1 + zz2) - (vv1 + uu1)).|| by A6, Def4
.= ||.((zz1 + zz2) + ((- uu1) + (- vv1))).|| by RLVECT_1:45
.= ||.(((zz1 + zz2) + (- vv1)) + (- uu1)).|| by RLVECT_1:def 6
.= ||.(((zz1 + (- vv1)) + zz2) + (- uu1)).|| by RLVECT_1:def 6
.= ||.((zz1 + (- vv1)) + (zz2 + (- uu1))).|| by RLVECT_1:def 6 ;
A8: ||.((zz1 - vv1) + (zz2 - uu1)).|| <= ||.(zz1 - vv1).|| + ||.(zz2 - uu1).|| by NORMSP_1:def 2;
A9: ( ||.(zz1 - vv1).|| = dist z1,v1 & ||.(zz2 - uu1).|| = dist z2,u1 ) by Def1;
( dist z1,v1 < r / 2 & dist z2,u1 < r / 2 ) by A6, METRIC_1:12;
then (dist z1,v1) + (dist z2,u1) < (r / 2) + (r / 2) by XREAL_1:10;
then dist z12,w1 < r by A7, A8, A9, XXREAL_0:2;
then w1 in Ball z12,r by METRIC_1:12;
hence w in V by A2; :: thesis:

end;

hence ex b₁, b₂ being Element of bool the carrier of (LinearTopSpaceNorm X) st
( b₁ is open & b₂ is open & x1 in b₁ & x2 in b₂ & b₁ + b₂ c= V ) by A3, A5; :: thesis:

end;

thus LinearTopSpaceNorm X is Mult-continuous :: thesis:

proof

let a be Real; :: according to RLTOPSP1:def 9 :: thesis:
let x be Point of (LinearTopSpaceNorm X); :: thesis:
let V be Subset of (LinearTopSpaceNorm X); :: thesis:
assume A10: ( V is open & a * x in V ) ; :: thesis:
reconsider z = x, az = a * x as Element of (MetricSpaceNorm X) by Def4;
reconsider z1 = z as Point of X ;
V in the topology of (LinearTopSpaceNorm X) by A10, PRE_TOPC:def 5;
then V in the topology of (TopSpaceNorm X) by Def4;
then consider r0 being Real such that
A11: ( r0 > 0 & Ball az,r0 c= V ) by A10, PCOMPS_1:def 5;
set r = r0 / 2;
set r2 = min (((r0 / 2) / 2) / ((1 + ||.z1.||) + (abs a))),1;
reconsider W = Ball z,(min (((r0 / 2) / 2) / ((1 + ||.z1.||) + (abs a))),1) as Subset of (LinearTopSpaceNorm X) by Def4;
Ball z,(min (((r0 / 2) / 2) / ((1 + ||.z1.||) + (abs a))),1) in the topology of (TopSpaceNorm X) by PCOMPS_1:33;
then Ball z,(min (((r0 / 2) / 2) / ((1 + ||.z1.||) + (abs a))),1) in the topology of (LinearTopSpaceNorm X) by Def4;
then A12: W is open by PRE_TOPC:def 5;
( 0 <= ||.z1.|| & 0 <= abs a ) by COMPLEX1:132, NORMSP_1:8;
then 0 <= ||.z1.|| + (abs a) ;
then A13: 0 < 1 + (||.z1.|| + (abs a)) ;
A14: r0 / 2 < r0 / 1 by A11, XREAL_1:78;
then ( r0 / 2 > 0 & r0 / 2 < r0 ) by A11, XREAL_1:217;
then A15: 0 < (r0 / 2) / 2 by XREAL_1:217;
then 0 / ((1 + ||.z1.||) + (abs a)) < ((r0 / 2) / 2) / ((1 + ||.z1.||) + (abs a)) by A13, XREAL_1:76;
then A16: 0 < min (((r0 / 2) / 2) / ((1 + ||.z1.||) + (abs a))),1 by XXREAL_0:15;
dist z,z = 0 by METRIC_1:1;
then A17: x in W by A16, METRIC_1:12;
for s being Real st abs (s - a) < min (((r0 / 2) / 2) / ((1 + ||.z1.||) + (abs a))),1 holds
s * W c= V

proof

let s be Real; :: thesis:
assume abs (s - a) < min (((r0 / 2) / 2) / ((1 + ||.z1.||) + (abs a))),1 ; :: thesis:
then A18: abs (a - s) <= min (((r0 / 2) / 2) / ((1 + ||.z1.||) + (abs a))),1 by COMPLEX1:146;
thus s * W c= V :: thesis:

proof

let w be set ; :: according to TARSKI:def 3 :: thesis:
assume w in s * W ; :: thesis:
then consider v being VECTOR of (LinearTopSpaceNorm X) such that
A19: ( w = s * v & v in W ) ;
reconsider v1 = v as Element of (MetricSpaceNorm X) by Def4;
reconsider w1 = w as Element of (MetricSpaceNorm X) by A19, Def4;
reconsider zza = a * x, zz = x, vv1 = v as Point of X by Def4;
reconsider ww1 = w as Point of X by A19, Def4;
A20: dist az,w1 = ||.(zza - ww1).|| by Def1
.= ||.((a * zz) - ww1).|| by Def4
.= ||.((a * zz) - (s * vv1)).|| by A19, Def4 ;
(a * (zz - vv1)) - ((s - a) * vv1) = ((a * zz) - (a * vv1)) - ((s - a) * vv1) by RLVECT_1:48
.= ((a * zz) - (a * vv1)) - ((s * vv1) - (a * vv1)) by RLVECT_1:49
.= (a * zz) - (((s * vv1) - (a * vv1)) + (a * vv1)) by RLVECT_1:41
.= (a * zz) - ((s * vv1) - ((a * vv1) - (a * vv1))) by RLVECT_1:43
.= (a * zz) - ((s * vv1) - (0. X)) by RLVECT_1:28
.= (a * zz) - (s * vv1) by RLVECT_1:26 ;
then ||.((a * zz) - (s * vv1)).|| <= ||.(a * (zz - vv1)).|| + ||.((s - a) * vv1).|| by NORMSP_1:7;
then ||.((a * zz) - (s * vv1)).|| <= ((abs a) * ||.(zz - vv1).||) + ||.((s - a) * vv1).|| by NORMSP_1:def 2;
then ||.((a * zz) - (s * vv1)).|| <= ((abs a) * ||.(zz - vv1).||) + ((abs (s - a)) * ||.vv1.||) by NORMSP_1:def 2;
then A21: ||.((a * zz) - (s * vv1)).|| <= ((abs a) * ||.(zz - vv1).||) + ((abs (a - s)) * ||.vv1.||) by COMPLEX1:146;
A22: ||.(zz - vv1).|| = dist z,v1 by Def1;
A23: dist z,v1 < min (((r0 / 2) / 2) / ((1 + ||.z1.||) + (abs a))),1 by A19, METRIC_1:12;
A24: 0 <= abs a by COMPLEX1:132;
then A25: ||.(zz - vv1).|| * (abs a) <= (min (((r0 / 2) / 2) / ((1 + ||.z1.||) + (abs a))),1) * (abs a) by A22, A23, XREAL_1:66;
(min (((r0 / 2) / 2) / ((1 + ||.z1.||) + (abs a))),1) * (abs a) <= (((r0 / 2) / 2) / ((1 + ||.z1.||) + (abs a))) * (abs a) by A24, XREAL_1:66, XXREAL_0:17;
then (abs a) * ||.(zz - vv1).|| <= (abs a) * (((r0 / 2) / 2) / ((1 + ||.z1.||) + (abs a))) by A25, XXREAL_0:2;
then A26: (abs a) * ||.(zz - vv1).|| <= ((abs a) / ((1 + ||.z1.||) + (abs a))) * ((r0 / 2) / 2) by XCMPLX_1:76;
0 <= 1 + ||.z1.|| by NORMSP_1:8, XREAL_1:41;
then 0 + (abs a) <= (1 + ||.z1.||) + (abs a) by XREAL_1:8;
then (abs a) / ((1 + ||.z1.||) + (abs a)) <= 1 by A24, XREAL_1:185;
then ((abs a) / ((1 + ||.z1.||) + (abs a))) * ((r0 / 2) / 2) <= 1 * ((r0 / 2) / 2) by A15, XREAL_1:66;
then A27: (abs a) * ||.(zz - vv1).|| <= (r0 / 2) / 2 by A26, XXREAL_0:2;
zz + (vv1 - zz) = vv1 - (zz - zz) by RLVECT_1:43
.= vv1 - (0. X) by RLVECT_1:28
.= vv1 by RLVECT_1:26 ;
then A28: ||.vv1.|| <= ||.zz.|| + ||.(vv1 - zz).|| by NORMSP_1:def 2;
min (((r0 / 2) / 2) / ((1 + ||.z1.||) + (abs a))),1 <= 1 by XXREAL_0:17;
then ||.(zz - vv1).|| <= 1 by A22, A23, XXREAL_0:2;
then ||.(vv1 - zz).|| <= 1 by NORMSP_1:11;
then ||.zz.|| + ||.(vv1 - zz).|| <= ||.zz.|| + 1 by XREAL_1:8;
then A29: ||.vv1.|| <= ||.zz.|| + 1 by A28, XXREAL_0:2;
( 0 <= abs (a - s) & 0 <= ||.vv1.|| ) by COMPLEX1:132, NORMSP_1:8;
then A30: (abs (a - s)) * ||.vv1.|| <= (min (((r0 / 2) / 2) / ((1 + ||.z1.||) + (abs a))),1) * (||.zz.|| + 1) by A18, A29, XREAL_1:68;
A31: 0 <= 1 + ||.z1.|| by NORMSP_1:8, XREAL_1:41;
then (min (((r0 / 2) / 2) / ((1 + ||.z1.||) + (abs a))),1) * (||.zz.|| + 1) <= (((r0 / 2) / 2) / ((1 + ||.z1.||) + (abs a))) * (||.zz.|| + 1) by XREAL_1:66, XXREAL_0:17;
then (abs (a - s)) * ||.vv1.|| <= (((r0 / 2) / 2) / ((1 + ||.z1.||) + (abs a))) * (||.z1.|| + 1) by A30, XXREAL_0:2;
then A32: (abs (a - s)) * ||.vv1.|| <= ((||.z1.|| + 1) / ((1 + ||.z1.||) + (abs a))) * ((r0 / 2) / 2) by XCMPLX_1:76;
0 <= abs a by COMPLEX1:132;
then 0 + (1 + ||.z1.||) <= (abs a) + (1 + ||.z1.||) by XREAL_1:8;
then (||.z1.|| + 1) / ((1 + ||.z1.||) + (abs a)) <= 1 by A31, XREAL_1:185;
then ((||.z1.|| + 1) / ((1 + ||.z1.||) + (abs a))) * ((r0 / 2) / 2) <= 1 * ((r0 / 2) / 2) by A15, XREAL_1:66;
then (abs (a - s)) * ||.vv1.|| <= (r0 / 2) / 2 by A32, XXREAL_0:2;
then ((abs a) * ||.(zz - vv1).||) + ((abs (a - s)) * ||.vv1.||) <= ((r0 / 2) / 2) + ((r0 / 2) / 2) by A27, XREAL_1:9;
then dist az,w1 <= r0 / 2 by A20, A21, XXREAL_0:2;
then dist az,w1 < r0 by A14, XXREAL_0:2;
then w1 in Ball az,r0 by METRIC_1:12;
hence w in V by A11; :: thesis:

end;

hence ex b₁ being Element of REAL ex b₂ being Element of bool the carrier of (LinearTopSpaceNorm X) st
( b₂ is open & x in b₂ & ( for b₃ being Element of REAL holds
( b₁ <= abs (b₃ - a) or b₃ * b₂ c= V ) ) ) by A12, A16, A17; :: thesis:

end;

thus LinearTopSpaceNorm X is TopSpace-like :: thesis:

proof

end;

thus LinearTopSpaceNorm X is Abelian :: thesis:

proof

let v, w be VECTOR of (LinearTopSpaceNorm X); :: according to RLVECT_1:def 5 :: thesis:
reconsider v1 = v, w1 = w as VECTOR of X by Def4;
thus v + w = v1 + w1 by Def4
.= w1 + v1
.= w + v by Def4 ; :: thesis:

end;

thus LinearTopSpaceNorm X is add-associative :: thesis:

proof

let v, w, x be VECTOR of (LinearTopSpaceNorm X); :: according to RLVECT_1:def 6 :: thesis:
reconsider v1 = v, w1 = w, x1 = x as VECTOR of X by Def4;
A37: ( v + w = v1 + w1 & w + x = w1 + x1 ) by Def4;
hence (v + w) + x = (v1 + w1) + x1 by Def4
.= v1 + (w1 + x1) by RLVECT_1:def 6
.= v + (w + x) by A37, Def4 ;
:: thesis:

end;

thus LinearTopSpaceNorm X is right_zeroed :: thesis:

proof

let v be VECTOR of (LinearTopSpaceNorm X); :: according to RLVECT_1:def 7 :: thesis:
reconsider v1 = v as VECTOR of X by Def4;
0. (LinearTopSpaceNorm X) = 0. X by Def4;
hence v + (0. (LinearTopSpaceNorm X)) = v1 + (0. X) by Def4
.= v by RLVECT_1:def 7 ;
:: thesis:

end;

thus LinearTopSpaceNorm X is right_complementable :: thesis:

proof

let v be VECTOR of (LinearTopSpaceNorm X); :: according to ALGSTR_0:def 16 :: thesis:
reconsider v1 = v as VECTOR of X by Def4;
reconsider w = - v1 as VECTOR of (LinearTopSpaceNorm X) by Def4;
take w ; :: according to ALGSTR_0:def 11 :: thesis:
thus v + w = v1 - v1 by Def4
.= 0. X by RLVECT_1:28
.= 0. (LinearTopSpaceNorm X) by Def4 ; :: thesis:

end;

thus LinearTopSpaceNorm X is RealLinearSpace-like :: thesis:

proof

A38: now

let a be Real; :: thesis:
let v, w be VECTOR of (LinearTopSpaceNorm X); :: thesis:
reconsider v1 = v, w1 = w as VECTOR of X by Def4;
( v + w = v1 + w1 & a * v = a * v1 & a * w = a * w1 ) by Def4;
then ( a * (v + w) = a * (v1 + w1) & (a * v1) + (a * w1) = (a * v) + (a * w) ) by Def4;
hence a * (v + w) = (a * v) + (a * w) by RLVECT_1:def 9; :: thesis:

end;

A39: now

let a, b be Real; :: thesis:
let v be VECTOR of (LinearTopSpaceNorm X); :: thesis:
reconsider v1 = v as VECTOR of X by Def4;
( a * v = a * v1 & b * v = b * v1 ) by Def4;
then ( (a + b) * v = (a + b) * v1 & (a * v1) + (b * v1) = (a * v) + (b * v) ) by Def4;
hence (a + b) * v = (a * v) + (b * v) by RLVECT_1:def 9; :: thesis:

end;

A40: now

let a, b be Real; :: thesis:
let v be VECTOR of (LinearTopSpaceNorm X); :: thesis:
reconsider v1 = v as VECTOR of X by Def4;
b * v = b * v1 by Def4;
then a * (b * v1) = a * (b * v) by Def4;
then (a * b) * v1 = a * (b * v) by RLVECT_1:def 9;
hence (a * b) * v = a * (b * v) by Def4; :: thesis:

end;

now

let v be VECTOR of (LinearTopSpaceNorm X); :: thesis:
reconsider v1 = v as VECTOR of X by Def4;
thus 1 * v = 1 * v1 by Def4
.= v by RLVECT_1:def 9 ; :: thesis:

end;

hence LinearTopSpaceNorm X is RealLinearSpace-like by A38, A39, A40, RLVECT_1:def 9; :: thesis:

end;