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;

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) )
;

end;

suppose A2:
p = 0. (TOP-REAL n)
; :: thesis: InnerProduct p is continuous

A3:
for q being Point of (TOP-REAL n) holds (InnerProduct p) . q = 0

A4: ( ( for p being Point of (TOP-REAL n) holds g . p = 0 ) & g is continuous ) by JGRAPH_2:20;

for x being object st x in the carrier of (TOP-REAL n) holds

(InnerProduct p) . x = g . x

end;proof

consider g being Function of (TOP-REAL n),R^1 such that
let q be Point of (TOP-REAL n); :: thesis: (InnerProduct p) . q = 0

(InnerProduct p) . q = |(q,p)| by Def1;

hence (InnerProduct p) . q = 0 by A2, EUCLID_2:32; :: thesis: verum

end;(InnerProduct p) . q = |(q,p)| by Def1;

hence (InnerProduct p) . q = 0 by A2, EUCLID_2:32; :: thesis: verum

A4: ( ( for p being Point of (TOP-REAL n) holds g . p = 0 ) & g is continuous ) by JGRAPH_2:20;

for x being object st x in the carrier of (TOP-REAL n) holds

(InnerProduct p) . x = g . x

proof

hence
InnerProduct p is continuous
by A4, FUNCT_2:12; :: thesis: verum
let x be object ; :: thesis: ( x in the carrier of (TOP-REAL n) implies (InnerProduct p) . x = g . x )

assume x in the carrier of (TOP-REAL n) ; :: thesis: (InnerProduct p) . x = g . x

then reconsider q = x as Point of (TOP-REAL n) ;

thus (InnerProduct p) . x = (InnerProduct p) . q

.= 0 by A3

.= g . q by A4

.= g . x ; :: thesis: verum

end;assume x in the carrier of (TOP-REAL n) ; :: thesis: (InnerProduct p) . x = g . x

then reconsider q = x as Point of (TOP-REAL n) ;

thus (InnerProduct p) . x = (InnerProduct p) . q

.= 0 by A3

.= g . q by A4

.= g . x ; :: thesis: verum

suppose
p <> 0. (TOP-REAL n)
; :: thesis: InnerProduct p is continuous

then A5:
|.p.| > 0
by EUCLID_2:44;

reconsider n1 = n as Element of NAT by ORDINAL1:def 12;

hence InnerProduct p is continuous by A1, PRE_TOPC:32, TOPMETR:def 6; :: thesis: verum

end;reconsider n1 = n as Element of NAT by ORDINAL1:def 12;

now :: thesis: 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 ) )

then
f1 is continuous
by UNIFORM1:3;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; :: thesis: 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); :: thesis: 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; :: thesis: ( 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 ; :: thesis: 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

( 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; :: thesis: verum

end;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); :: thesis: 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; :: thesis: ( 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 ; :: thesis: 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

hence
ex s being Real st
let w be Element of (Euclid n); :: thesis: for w1 being Element of RealSpace st w1 = f1 . w & dist (u,w) < r / |.p.| holds

dist (u1,w1) < r

let w1 be Element of RealSpace; :: thesis: ( 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.| ; :: thesis: 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; :: thesis: verum

end;dist (u1,w1) < r

let w1 be Element of RealSpace; :: thesis: ( 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.| ; :: thesis: 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; :: thesis: verum

( 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; :: thesis: verum

hence InnerProduct p is continuous by A1, PRE_TOPC:32, TOPMETR:def 6; :: thesis: verum