set f = InnerProduct p;
A1: TopStruct(# the carrier of (), the topology of () #) = TopSpaceMetr () by EUCLID:def 8;
then reconsider f1 = InnerProduct p as Function of (), by TOPMETR:def 6;
per cases ( p = 0. () or p <> 0. () ) ;
suppose A2: p = 0. () ; :: thesis:
A3: for q being Point of () holds () . q = 0
proof
let q be Point of (); :: thesis: () . q = 0
(InnerProduct p) . q = |(q,p)| by Def1;
hence (InnerProduct p) . q = 0 by ; :: thesis: verum
end;
consider g being Function of (),R^1 such that
A4: ( ( for p being Point of () holds g . p = 0 ) & g is continuous ) by JGRAPH_2:20;
for x being object st x in the carrier of () holds
() . x = g . x
proof
let x be object ; :: thesis: ( x in the carrier of () implies () . x = g . x )
assume x in the carrier of () ; :: thesis: () . x = g . x
then reconsider q = x as Point of () ;
thus () . x = () . q
.= 0 by A3
.= g . q by A4
.= g . x ; :: thesis: verum
end;
hence InnerProduct p is continuous by ; :: thesis: verum
end;
suppose p <> 0. () ; :: thesis:
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 ()
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 ()
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 ()
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 ()
for w1 being Element of RealSpace st w1 = f1 . w & dist (u,w) < s holds
dist (u1,w1) < r ) )

let u be Element of (); :: 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 ()
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 ()
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 ()
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 ()
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 (); :: 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 ;
A11: w1 = |(qw,p)| by ;
|.(tu - tw).| = |.(|(qu,p)| - |(qw,p)|).| by
.= |.|((qu - qw),p)|.| by EUCLID_2:24 ;
then A12: dist (u1,w1) <= |.(qu - qw).| * |.p.| by ;
A13: (dist (u,w)) * |.p.| = |.(qu - qw).| * |.p.| by JGRAPH_1:28;
(dist (u,w)) * |.p.| < (r / |.p.|) * |.p.| by ;
then (dist (u,w)) * |.p.| < r / () by XCMPLX_1:82;
then (dist (u,w)) * |.p.| < r / 1 by ;
hence dist (u1,w1) < r by ; :: thesis: verum
end;
hence ex s being Real st
( s > 0 & ( for w being Element of ()
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 ; :: thesis: verum
end;
end;