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 |.s.| < r holds
s * V c= U and
A2: F = { (a * V) where a is Real : |.a.| < r } ; :: thesis:
set W = union F;
thus union F is a_neighborhood of 0. X :: thesis:

set F9 = { (a * (Int V)) where a is non zero Real : |.a.| < r } ;
consider a being Real such that
A3: 0 < a and
A4: a < r by XREAL_1:5;
reconsider a = a as Real ;
0. X in Int V by CONNSP_2:def 1;
then a * (0. X) in a * (Int V) ;
then A5: 0. X in a * (Int V) ;
A6: { (a * (Int V)) where a is non zero Real : |.a.| < r } c= bool the carrier of X

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

end;

|.a.| < r by A3, A4, ABSVALUE:def 1;
then a * (Int V) in { (a * (Int V)) where a is non zero Real : |.a.| < r } by A3;
then A7: 0. X in union { (a * (Int V)) where a is non zero Real : |.a.| < r } by A5, TARSKI:def 4;
reconsider F9 = { (a * (Int V)) where a is non zero Real : |.a.| < r } as Subset-Family of X by A6;
union F9 c= union F

let x be object ; :: according to TARSKI:def 3 :: thesis:
A8: Int V c= V by TOPS_1:16;
assume x in union F9 ; :: thesis:
then consider P being set such that
A9: x in P and
A10: P in F9 by TARSKI:def 4;
consider a being non zero Real such that
A11: P = a * (Int V) and
A12: |.a.| < r by A10;
ex v being Point of X st
( x = a * v & v in Int V ) by A9, A11;
then A13: x in a * V by A8;
a * V in F by A2, A12;
hence x in union F by A13, TARSKI:def 4; :: thesis:

end;

end;

end;

let s be Real; :: according to RLTOPSP1:def 6 :: thesis:
assume |.s.| <= 1 ; :: thesis:
then A15: |.s.| * r <= r by XREAL_1:153;
let z be object ; :: according to TARSKI:def 3 :: thesis:
assume z in s * (union F) ; :: thesis:
then consider u being Point of X such that
A16: z = s * u and
A17: u in union F ;
consider Y being set such that
A18: u in Y and
A19: Y in F by A17, TARSKI:def 4;
consider a being Real such that
A20: Y = a * V and
A21: |.a.| < r by A2, A19;
consider v being Point of X such that
A22: u = a * v and
A23: v in V by A18, A20;
z = (s * a) * v by A16, A22, RLVECT_1:def 7;
then A24: z in (s * a) * V by A23;

end;

end;

let z be object ; :: according to TARSKI:def 3 :: thesis:
assume A25: z in union F ; :: thesis:
then reconsider z = z as Point of X ;
consider Y being set such that
A26: z in Y and
A27: Y in F by A25, TARSKI:def 4;
consider a being Real such that
A28: Y = a * V and
A29: |.a.| < r by A2, A27;
a * V c= U by A1, A29;
hence z in U by A26, A28; :: thesis: