set ZS = {0};
set T = {{},{0}};
{{},{0}} c= bool {0}

let x be object ; :: according to TARSKI:def 3 :: thesis:
reconsider xx = x as set by TARSKI:1;
assume x in {{},{0}} ; :: thesis:
then ( x = {} or x = {0} ) by TARSKI:def 2;
then xx c= {0} ;
hence x in bool {0} ; :: thesis:

end;

then reconsider T = {{},{0}} as Subset-Family of {0} ;
reconsider O = 0 as Element of {0} by TARSKI:def 1;
deffunc H₁( Element of {0}, Element of {0}) -> Element of {0} = O;
consider F being BinOp of {0} such that
A1: for x, y being Element of {0} holds F . (x,y) = H₁(x,y) from BINOP_1:sch 4();
deffunc H₂( Real, Element of {0}) -> Element of {0} = O;
consider G being Function of [:REAL,{0}:],{0} such that
A2: for a being Element of REAL
for x being Element of {0} holds G . (a,x) = H₂(a,x) from BINOP_1:sch 4();
take W = RLTopStruct(# {0},O,F,G,T #); :: thesis:
thus W is strict ; :: thesis:
thus W is add-continuous :: thesis:

proof

reconsider V1 = {O}, V2 = {O} as Subset of W ;
let x1, x2 be Point of W; :: according to RLTOPSP1:def 8 :: thesis:
let V be Subset of W; :: thesis:
assume that
A3: V is open and
A4: x1 + x2 in V ; :: thesis:
take V1 ; :: thesis:
take V2 ; :: thesis:
V1 in T by TARSKI:def 2;
hence ( V1 is open & V2 is open ) ; :: thesis:
thus ( x1 in V1 & x2 in V2 ) ; :: thesis:
V in T by A3;
then V = the carrier of W by A4, TARSKI:def 2;
hence V1 + V2 c= V ; :: thesis:

end;

thus W is Mult-continuous :: thesis:

proof

reconsider V9 = {O} as Subset of W ;
let a be Real; :: according to RLTOPSP1:def 9 :: thesis:
let x be Point of W; :: thesis:
let V be Subset of W; :: thesis:
assume that
A5: V is open and
A6: a * x in V ; :: thesis:
take jj ; :: thesis:
take V9 ; :: thesis:
V9 in T by TARSKI:def 2;
hence V9 is open ; :: thesis:
thus x in V9 ; :: thesis:
let s be Real; :: thesis:
assume |.(s - a).| < jj ; :: thesis:
V in T by A5;
then ( V = {} or V = {0} ) by TARSKI:def 2;
hence s * V9 c= V by A6; :: thesis:

end;

thus W is TopSpace-like :: thesis:

proof

thus the carrier of W in the topology of W by TARSKI:def 2; :: according to PRE_TOPC:def 1 :: thesis:

hereby :: thesis:

let a be Subset-Family of W; :: thesis:
assume a c= the topology of W ; :: thesis:
then ( a = {} or a = {{}} or a = {{0}} or a = {{},{0}} ) by ZFMISC_1:36;
then ( union a = {} or union a = {0} or union a = {} \/ {0} ) by ZFMISC_1:2, ZFMISC_1:25, ZFMISC_1:75;
hence union a in the topology of W by TARSKI:def 2; :: thesis:

end;

let a, b be Subset of W; :: thesis:
assume that
A7: a in the topology of W and
A8: b in the topology of W ; :: thesis:
A9: ( b = {} or b = {0} ) by A8, TARSKI:def 2;
( a = {} or a = {0} ) by A7, TARSKI:def 2;
hence a /\ b in the topology of W by A9, TARSKI:def 2; :: thesis:

end;

thus for x, y being Point of W holds x + y = y + x :: according to RLVECT_1:def 2 :: thesis:

proof

let x, y be Point of W; :: thesis:
reconsider X = x, Y = y as Element of {0} ;
x + y = H₁(X,Y) by A1;
hence x + y = y + x by A1; :: thesis:

end;

thus for x, y, z being Point of W holds (x + y) + z = x + (y + z) :: according to RLVECT_1:def 3 :: thesis:

proof

let x, y, z be Point of W; :: thesis:
reconsider X = x, Y = y, Z = z as Element of {0} ;
(x + y) + z = H₁(H₁(X,Y),Z) by A1;
hence (x + y) + z = x + (y + z) by A1; :: thesis:

end;

thus for x being Point of W holds x + (0. W) = x :: according to RLVECT_1:def 4 :: thesis:

proof

let x be Point of W; :: thesis:
reconsider X = x as Element of {0} ;
x + (0. W) = H₁(X,O) by A1;
hence x + (0. W) = x by TARSKI:def 1; :: thesis:

end;

thus for x being Point of W holds x is right_complementable :: according to ALGSTR_0:def 16 :: thesis:

proof

reconsider y = O as Point of W ;
let x be Point of W; :: thesis:
take y ; :: according to ALGSTR_0:def 11 :: thesis:
thus x + y = 0. W by A1; :: thesis:

end;

thus for a being Real
for x, y being Point of W holds a * (x + y) = (a * x) + (a * y) :: according to RLVECT_1:def 5 :: thesis:

proof

let a be Real; :: thesis:
reconsider a = a as Element of REAL by XREAL_0:def 1;
let x, y be Point of W; :: thesis:
reconsider X = x, Y = y as Element of {0} ;
(a * x) + (a * y) = H₂(a,H₁(X,Y)) by A1
.= G . (a,H₁(X,Y)) by A2
.= G . (a,(F . (x,y))) by A1 ;
hence a * (x + y) = (a * x) + (a * y) ; :: thesis:

end;

thus for a, b being Real
for x being Point of W holds (a + b) * x = (a * x) + (b * x) :: according to RLVECT_1:def 6 :: thesis:

proof

let a, b be Real; :: thesis:
let x be Point of W; :: thesis:
reconsider a = a, b = b as Element of REAL by XREAL_0:def 1;
set c = a + b;
reconsider X = x as Element of {0} ;
(a + b) * x = H₂(a + b,X) by A2;
hence (a + b) * x = (a * x) + (b * x) by A1; :: thesis:

end;

thus for a, b being Real
for x being Point of W holds (a * b) * x = a * (b * x) :: according to RLVECT_1:def 7 :: thesis:

proof

let a, b be Real; :: thesis:
let x be Point of W; :: thesis:
reconsider a = a, b = b as Element of REAL by XREAL_0:def 1;
set c = a * b;
reconsider X = x as Element of {0} ;
(a * b) * x = H₂(a * b,X) by A2;
hence (a * b) * x = a * (b * x) by A2; :: thesis:

end;

thus for x being Point of W holds 1 * x = x :: according to RLVECT_1:def 8 :: thesis:

proof

reconsider A9 = 1 as Element of REAL by XREAL_0:def 1;
let x be Point of W; :: thesis:
reconsider X = x as Element of {0} ;
A9 * x = H₂(A9,X) by A2;
hence 1 * x = x by TARSKI:def 1; :: thesis:

end;