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

let x be set ; :: according to TARSKI:def 3 :: thesis:
assume x in {{} ,{0 }} ; :: thesis:
then ( x = {} or x = {0 } ) by TARSKI:def 2;
then x c= {0 } by XBOOLE_1:2;
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 number , 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 ) by PRE_TOPC:def 5; :: thesis:
thus ( x1 in V1 & x2 in V2 ) ; :: thesis:
V in T by A3, PRE_TOPC:def 5;
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 1 ; :: thesis:
take V9 ; :: thesis:
V9 in T by TARSKI:def 2;
hence V9 is open by PRE_TOPC:def 5; :: thesis:
thus x in V9 ; :: thesis:
let s be Real; :: thesis:
assume abs (s - a) < 1 ; :: thesis:
V in T by A5, PRE_TOPC:def 5;
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:42;
then ( union a = {} or union a = {0 } or union a = {} \/ {0 } ) by ZFMISC_1:2, ZFMISC_1:31, ZFMISC_1:93;
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 5 :: 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 6 :: 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 7 :: 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 number
for x, y being Point of W holds a * (x + y) = (a * x) + (a * y) :: according to RLVECT_1:def 8 :: thesis:

proof

let a be real number ; :: thesis:
reconsider a = a as 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 number
for x being Point of W holds (a + b) * x = (a * x) + (b * x) :: according to RLVECT_1:def 9 :: thesis:

proof

let a, b be real number ; :: thesis:
let x be Point of W; :: thesis:
reconsider a = a, b = b as 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 number
for x being Point of W holds (a * b) * x = a * (b * x) :: according to RLVECT_1:def 10 :: thesis:

proof

let a, b be real number ; :: thesis:
let x be Point of W; :: thesis:
reconsider a = a, b = b as 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 11 :: thesis:

proof

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

end;