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

proof

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;

consider g being Function of (TOP-REAL n),R^1 such that
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

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;

hence InnerProduct p is continuous by A4, FUNCT_2:12; :: thesis: verum

end;

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;

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

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

proof

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;

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

end;

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

end;

end;