let X be LinearTopSpace; :: thesis:
let U, V be a_neighborhood of 0. X; :: thesis:
let F be Subset-Family of X; :: thesis:
let r be positive Real; :: thesis:
assume that
A1: for s being Real st abs s < r holds
s * V c= U and
A2: F = { (a * V) where a is Real : abs a < r } ; :: thesis:
set W = union F;
thus union F is a_neighborhood of 0. X :: thesis:

set F' = { (a * (Int V)) where a is non zero Real : abs a < r } ;
consider a being real number such that
A3: 0 < a and
A4: a < r by XREAL_1:7;
reconsider a = a as Real by XREAL_0:def 1;
A5: abs a < r by A3, A4, ABSVALUE:def 1;
A6: 0. X in Int V by CONNSP_2:def 1;
A7: a * (Int V) in { (a * (Int V)) where a is non zero Real : abs a < r } by A3, A5;
a * (0. X) in a * (Int V) by A6;
then 0. X in a * (Int V) by RLVECT_1:23;
then A8: 0. X in union { (a * (Int V)) where a is non zero Real : abs a < r } by A7, TARSKI:def 4;
{ (a * (Int V)) where a is non zero Real : abs a < r } c= bool the carrier of X

let A be set ; :: according to TARSKI:def 3 :: thesis:
assume A in { (a * (Int V)) where a is non zero Real : abs a < r } ; :: thesis:
then ex a being non zero Real st
( A = a * (Int V) & abs a < r ) ;
hence A in bool the carrier of X ; :: thesis:

end;

then reconsider F' = { (a * (Int V)) where a is non zero Real : abs a < r } as Subset-Family of X ;
F' is open

let P be Subset of X; :: according to TOPS_2:def 1 :: thesis:
assume P in F' ; :: thesis:
then ex a being non zero Real st
( P = a * (Int V) & abs a < r ) ;
hence P is open by Th50; :: thesis:

end;

then union F' is open by TOPS_2:26;
then A9: 0. X in Int (union F') by A8, TOPS_1:55;
union F' c= union F

let x be set ; :: according to TARSKI:def 3 :: thesis:
assume x in union F' ; :: thesis:
then consider P being set such that
A10: x in P and
A11: P in F' by TARSKI:def 4;
consider a being non zero Real such that
A12: P = a * (Int V) and
A13: abs a < r by A11;
consider v being Point of X such that
A14: x = a * v and
A15: v in Int V by A10, A12;
A16: Int V c= V by TOPS_1:44;
A17: a * V in F by A2, A13;
x in a * V by A14, A15, A16;
hence x in union F by A17, TARSKI:def 4; :: thesis:

end;

then Int (union F') c= Int (union F) by TOPS_1:48;
hence 0. X in Int (union F) by A9; :: according to CONNSP_2:def 1 :: thesis:

end;

thus union F is circled :: thesis:

let s be Real; :: according to RLTOPSP1:def 6 :: thesis:
assume A18: abs s <= 1 ; :: thesis:
let z be set ; :: according to TARSKI:def 3 :: thesis:
assume z in s * (union F) ; :: thesis:
then consider u being Point of X such that
A19: z = s * u and
A20: u in union F ;
consider Y being set such that
A21: u in Y and
A22: Y in F by A20, TARSKI:def 4;
consider a being Real such that
A23: Y = a * V and
A24: abs a < r by A2, A22;
consider v being Point of X such that
A25: u = a * v and
A26: v in V by A21, A23;
z = (s * a) * v by A19, A25, RLVECT_1:def 9;
then A27: z in (s * a) * V by A26;
A28: (abs s) * r <= r by A18, XREAL_1:155;

per cases ;

suppose 0 <> abs s ; :: thesis:

then s <> 0 by ABSVALUE:7;
then 0 < abs s by COMPLEX1:133;
then (abs s) * (abs a) < (abs s) * r by A24, XREAL_1:70;
then (abs s) * (abs a) < r by A28, XXREAL_0:2;
then abs (s * a) < r by COMPLEX1:151;
then (s * a) * V in F by A2;
hence z in union F by A27, TARSKI:def 4; :: thesis:

end;

suppose abs s = 0 ; :: thesis:

then s = 0 by ABSVALUE:7;
then abs (s * a) = 0 by ABSVALUE:def 1;
then (s * a) * V in F by A2;
hence z in union F by A27, TARSKI:def 4; :: thesis:

end;

let z be set ; :: according to TARSKI:def 3 :: thesis:
assume A29: z in union F ; :: thesis:
then reconsider z = z as Point of X ;
consider Y being set such that
A30: z in Y and
A31: Y in F by A29, TARSKI:def 4;
consider a being Real such that
A32: Y = a * V and
A33: abs a < r by A2, A31;
a * V c= U by A1, A33;
hence z in U by A30, A32; :: thesis: