let m, n be Nat; for s being Function of [:NAT,NAT:],(TopSpaceMetr (Euclid 1))
for y being Point of (Euclid 1) holds
( s .: (square-uparrow n) c= { q where q is Element of (Euclid 1) : dist (y,q) < 1 / m } iff for x being object st x in s .: (square-uparrow n) holds
ex rx, ry being Real st
( x = <*rx*> & y = <*ry*> & |.(ry - rx).| < 1 / m ) )
let s be Function of [:NAT,NAT:],(TopSpaceMetr (Euclid 1)); for y being Point of (Euclid 1) holds
( s .: (square-uparrow n) c= { q where q is Element of (Euclid 1) : dist (y,q) < 1 / m } iff for x being object st x in s .: (square-uparrow n) holds
ex rx, ry being Real st
( x = <*rx*> & y = <*ry*> & |.(ry - rx).| < 1 / m ) )
let y be Point of (Euclid 1); ( s .: (square-uparrow n) c= { q where q is Element of (Euclid 1) : dist (y,q) < 1 / m } iff for x being object st x in s .: (square-uparrow n) holds
ex rx, ry being Real st
( x = <*rx*> & y = <*ry*> & |.(ry - rx).| < 1 / m ) )
hereby ( ( for x being object st x in s .: (square-uparrow n) holds
ex rx, ry being Real st
( x = <*rx*> & y = <*ry*> & |.(ry - rx).| < 1 / m ) ) implies s .: (square-uparrow n) c= { q where q is Element of (Euclid 1) : dist (y,q) < 1 / m } )
assume A1:
s .: (square-uparrow n) c= { q where q is Element of (Euclid 1) : dist (y,q) < 1 / m }
;
for x being object st x in s .: (square-uparrow n) holds
ex rx, ry being Real st
( x = <*rx*> & y = <*ry*> & |.(ry - rx).| < 1 / m )now for x being object st x in s .: (square-uparrow n) holds
ex rx, ry being Real st
( x = <*rx*> & y = <*ry*> & |.(ry - rx).| < 1 / m )let x be
object ;
( x in s .: (square-uparrow n) implies ex rx, ry being Real st
( x = <*rx*> & y = <*ry*> & |.(ry - rx).| < 1 / m ) )assume A2:
x in s .: (square-uparrow n)
;
ex rx, ry being Real st
( x = <*rx*> & y = <*ry*> & |.(ry - rx).| < 1 / m )then consider yo being
object such that A3:
yo in dom s
and
yo in square-uparrow n
and A4:
x = s . yo
by FUNCT_1:def 6;
reconsider z =
x as
Element of
(Euclid 1) by A3, A4, FUNCT_2:5;
z in { q where q is Element of (Euclid 1) : dist (y,q) < 1 / m }
by A2, A1;
then consider q being
Element of
(Euclid 1) such that A5:
z = q
and A6:
dist (
y,
q)
< 1
/ m
;
reconsider yr1 =
y as
Point of
(Euclid 1) ;
yr1 in 1
-tuples_on REAL
;
then
yr1 in { <*r*> where r is Element of REAL : verum }
by FINSEQ_2:96;
then consider ry being
Element of
REAL such that A8:
yr1 = <*ry*>
;
reconsider zr1 =
z as
Point of
(Euclid 1) ;
zr1 in 1
-tuples_on REAL
;
then
zr1 in { <*r*> where r is Element of REAL : verum }
by FINSEQ_2:96;
then consider rx being
Element of
REAL such that A9:
zr1 = <*rx*>
;
|.(ry - rx).| < 1
/ m
by A5, A6, A8, A9, Th8;
hence
ex
rx,
ry being
Real st
(
x = <*rx*> &
y = <*ry*> &
|.(ry - rx).| < 1
/ m )
by A8, A9;
verum end; hence
for
x being
object st
x in s .: (square-uparrow n) holds
ex
rx,
ry being
Real st
(
x = <*rx*> &
y = <*ry*> &
|.(ry - rx).| < 1
/ m )
;
verum
end;
assume A10:
for x being object st x in s .: (square-uparrow n) holds
ex rx, ry being Real st
( x = <*rx*> & y = <*ry*> & |.(ry - rx).| < 1 / m )
; s .: (square-uparrow n) c= { q where q is Element of (Euclid 1) : dist (y,q) < 1 / m }
now for t being object st t in s .: (square-uparrow n) holds
t in { q where q is Element of (Euclid 1) : dist (y,q) < 1 / m } let t be
object ;
( t in s .: (square-uparrow n) implies t in { q where q is Element of (Euclid 1) : dist (y,q) < 1 / m } )assume A11:
t in s .: (square-uparrow n)
;
t in { q where q is Element of (Euclid 1) : dist (y,q) < 1 / m } then consider rx,
ry being
Real such that A12:
t = <*rx*>
and A13:
y = <*ry*>
and A14:
|.(ry - rx).| < 1
/ m
by A10;
consider yo being
object such that A15:
yo in dom s
and
yo in square-uparrow n
and A16:
t = s . yo
by A11, FUNCT_1:def 6;
reconsider q =
t as
Element of
(Euclid 1) by A15, A16, FUNCT_2:5;
dist (
y,
q)
< 1
/ m
by A12, A13, A14, Th8;
hence
t in { q where q is Element of (Euclid 1) : dist (y,q) < 1 / m }
;
verum end;
hence
s .: (square-uparrow n) c= { q where q is Element of (Euclid 1) : dist (y,q) < 1 / m }
; verum