set f = InnerProduct p;
A1:
TopStruct(# the carrier of (TOP-REAL n), the topology of (TOP-REAL n) #) = TopSpaceMetr (Euclid n)
by EUCLID:def 8;
then reconsider f1 = InnerProduct p as Function of (TopSpaceMetr (Euclid n)),(TopSpaceMetr RealSpace) by TOPMETR:def 6;
per cases
( p = 0. (TOP-REAL n) or p <> 0. (TOP-REAL n) )
;
suppose
p <> 0. (TOP-REAL n)
;
InnerProduct p is continuous then A5:
|.p.| > 0
by EUCLID_2:44;
reconsider n1 =
n as
Element of
NAT by ORDINAL1:def 12;
now for r being Real
for u being Element of (Euclid n)
for u1 being Element of RealSpace st r > 0 & u1 = f1 . u holds
ex s being Real st
( s > 0 & ( for w being Element of (Euclid n)
for w1 being Element of RealSpace st w1 = f1 . w & dist (u,w) < s holds
dist (u1,w1) < r ) )let r be
Real;
for u being Element of (Euclid n)
for u1 being Element of RealSpace st r > 0 & u1 = f1 . u holds
ex s being Real st
( s > 0 & ( for w being Element of (Euclid n)
for w1 being Element of RealSpace st w1 = f1 . w & dist (u,w) < s holds
dist (u1,w1) < r ) )let u be
Element of
(Euclid n);
for u1 being Element of RealSpace st r > 0 & u1 = f1 . u holds
ex s being Real st
( s > 0 & ( for w being Element of (Euclid n)
for w1 being Element of RealSpace st w1 = f1 . w & dist (u,w) < s holds
dist (u1,w1) < r ) )let u1 be
Element of
RealSpace;
( r > 0 & u1 = f1 . u implies ex s being Real st
( s > 0 & ( for w being Element of (Euclid n)
for w1 being Element of RealSpace st w1 = f1 . w & dist (u,w) < s holds
dist (u1,w1) < r ) ) )assume that A6:
r > 0
and A7:
u1 = f1 . u
;
ex s being Real st
( s > 0 & ( for w being Element of (Euclid n)
for w1 being Element of RealSpace st w1 = f1 . w & dist (u,w) < s holds
dist (u1,w1) < r ) )set s1 =
r / |.p.|;
for
w being
Element of
(Euclid n) for
w1 being
Element of
RealSpace st
w1 = f1 . w &
dist (
u,
w)
< r / |.p.| holds
dist (
u1,
w1)
< r
proof
let w be
Element of
(Euclid n);
for w1 being Element of RealSpace st w1 = f1 . w & dist (u,w) < r / |.p.| holds
dist (u1,w1) < rlet w1 be
Element of
RealSpace;
( w1 = f1 . w & dist (u,w) < r / |.p.| implies dist (u1,w1) < r )
assume that A8:
w1 = f1 . w
and A9:
dist (
u,
w)
< r / |.p.|
;
dist (u1,w1) < r
reconsider tu =
u1,
tw =
w1 as
Real by METRIC_1:def 13;
reconsider qw =
w,
qu =
u as
Point of
(TOP-REAL n1) by TOPREAL3:8;
A10:
dist (
u1,
w1) =
the
distance of
RealSpace . (
u1,
w1)
by METRIC_1:def 1
.=
|.(tu - tw).|
by METRIC_1:def 12, METRIC_1:def 13
;
A11:
w1 = |(qw,p)|
by Def1, A8;
|.(tu - tw).| =
|.(|(qu,p)| - |(qw,p)|).|
by Def1, A7, A11
.=
|.|((qu - qw),p)|.|
by EUCLID_2:24
;
then A12:
dist (
u1,
w1)
<= |.(qu - qw).| * |.p.|
by A10, EUCLID_2:51;
A13:
(dist (u,w)) * |.p.| = |.(qu - qw).| * |.p.|
by JGRAPH_1:28;
(dist (u,w)) * |.p.| < (r / |.p.|) * |.p.|
by A9, A5, XREAL_1:68;
then
(dist (u,w)) * |.p.| < r / (|.p.| / |.p.|)
by XCMPLX_1:82;
then
(dist (u,w)) * |.p.| < r / 1
by A5, XCMPLX_1:60;
hence
dist (
u1,
w1)
< r
by A13, A12, XXREAL_0:2;
verum
end; hence
ex
s being
Real st
(
s > 0 & ( for
w being
Element of
(Euclid n) for
w1 being
Element of
RealSpace st
w1 = f1 . w &
dist (
u,
w)
< s holds
dist (
u1,
w1)
< r ) )
by A5, A6;
verum end; then
f1 is
continuous
by UNIFORM1:3;
hence
InnerProduct p is
continuous
by A1, PRE_TOPC:32, TOPMETR:def 6;
verum end; end;