per cases ( not n is zero or n is zero ) ;
suppose not n is zero ; :: thesis:
then reconsider n = n as non zero Element of NAT by ORDINAL1:def 12;
set T = TOP-REAL n;
set F = TIMES n;
set J = (Seg n) --> R^1;
set c = the carrier of ();
A1: TopSpaceMetr () = product ((Seg n) --> R^1) by EUCLID_9:28;
A2: TopStruct(# the carrier of (), the topology of () #) = TopSpaceMetr () by EUCLID:def 8;
then reconsider F = TIMES n as Function of [:(),():],(product ((Seg n) --> R^1)) by EUCLID_9:28;
A3: the carrier of () = REAL n by EUCLID:22;
now :: thesis: for i being Element of Seg n holds (proj (((Seg n) --> R^1),i)) * F is continuous
let i be Element of Seg n; :: thesis: (proj (((Seg n) --> R^1),i)) * F is continuous
set P = proj (((Seg n) --> R^1),i);
reconsider f = (proj (((Seg n) --> R^1),i)) * F as Function of [:(),():],R^1 ;
A5: the carrier of [:(),():] = [: the carrier of (), the carrier of ():] by BORSUK_1:def 2;
A6: for a, b being Point of () holds f . (a,b) = (a . i) * (b . i)
proof
let a, b be Point of (); :: thesis: f . (a,b) = (a . i) * (b . i)
thus f . (a,b) = (proj (((Seg n) --> R^1),i)) . (F . (a,b)) by
.= (proj (((Seg n) --> R^1),i)) . (a (#) b) by Def5
.= (a (#) b) . i by
.= (a . i) * (b . i) by VALUED_1:5 ; :: thesis: verum
end;
deffunc H1( Element of the carrier of (), Element of the carrier of ()) -> Element of REAL = In ((n . i),REAL);
consider f1 being Function of [: the carrier of (), the carrier of ():],REAL such that
A7: for a, b being Element of the carrier of () holds f1 . (a,b) = H1(a,b) from reconsider f1 = f1 as Function of [:(),():],R^1 by A5;
deffunc H2( Element of the carrier of (), Element of the carrier of ()) -> Element of REAL = In ((c2 . i),REAL);
consider f2 being Function of [: the carrier of (), the carrier of ():],REAL such that
A8: for a, b being Element of the carrier of () holds f2 . (a,b) = H2(a,b) from reconsider f1 = f1, f2 = f2 as Function of [:(),():],R^1 by A5;
for p being Point of [:(),():]
for r being positive Real ex W being open Subset of [:(),():] st
( p in W & f1 .: W c= ].((f1 . p) - r),((f1 . p) + r).[ )
proof
let p be Point of [:(),():]; :: thesis: for r being positive Real ex W being open Subset of [:(),():] st
( p in W & f1 .: W c= ].((f1 . p) - r),((f1 . p) + r).[ )

let r be positive Real; :: thesis: ex W being open Subset of [:(),():] st
( p in W & f1 .: W c= ].((f1 . p) - r),((f1 . p) + r).[ )

consider p1, p2 being Point of () such that
A9: p = [p1,p2] by BORSUK_1:10;
set B1 = Ball (p1,r);
set B2 = [#] ();
reconsider W = [:(Ball (p1,r)),([#] ()):] as open Subset of [:(),():] by BORSUK_1:6;
take W ; :: thesis: ( p in W & f1 .: W c= ].((f1 . p) - r),((f1 . p) + r).[ )
( p1 in Ball (p1,r) & p2 in [#] () ) by TOPGEN_5:13;
hence p in W by ; :: thesis: f1 .: W c= ].((f1 . p) - r),((f1 . p) + r).[
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in f1 .: W or y in ].((f1 . p) - r),((f1 . p) + r).[ )
assume y in f1 .: W ; :: thesis: y in ].((f1 . p) - r),((f1 . p) + r).[
then consider x being Point of [:(),():] such that
A10: x in W and
A11: f1 . x = y by FUNCT_2:65;
consider x1, x2 being Point of () such that
A12: x = [x1,x2] by BORSUK_1:10;
A13: ( f1 . (x1,x2) = H1(x1,x2) & f1 . (p1,p2) = H1(p1,p2) ) by A7;
x1 in Ball (p1,r) by ;
then A14: |.(x1 - p1).| < r by TOPREAL9:7;
dom (x1 - p1) = Seg n by FINSEQ_1:89;
then (x1 . i) - (p1 . i) = (x1 - p1) . i by VALUED_1:13;
then |.((x1 . i) - (p1 . i)).| <= |.(x1 - p1).| by ;
then |.((f1 . x) - (f1 . p)).| < r by ;
hence y in ].((f1 . p) - r),((f1 . p) + r).[ by ; :: thesis: verum
end;
then A15: f1 is continuous by TOPS_4:21;
for p being Point of [:(),():]
for r being positive Real ex W being open Subset of [:(),():] st
( p in W & f2 .: W c= ].((f2 . p) - r),((f2 . p) + r).[ )
proof
let p be Point of [:(),():]; :: thesis: for r being positive Real ex W being open Subset of [:(),():] st
( p in W & f2 .: W c= ].((f2 . p) - r),((f2 . p) + r).[ )

let r be positive Real; :: thesis: ex W being open Subset of [:(),():] st
( p in W & f2 .: W c= ].((f2 . p) - r),((f2 . p) + r).[ )

consider p1, p2 being Point of () such that
A16: p = [p1,p2] by BORSUK_1:10;
set B1 = [#] ();
set B2 = Ball (p2,r);
reconsider W = [:([#] ()),(Ball (p2,r)):] as open Subset of [:(),():] by BORSUK_1:6;
take W ; :: thesis: ( p in W & f2 .: W c= ].((f2 . p) - r),((f2 . p) + r).[ )
( p1 in [#] () & p2 in Ball (p2,r) ) by TOPGEN_5:13;
hence p in W by ; :: thesis: f2 .: W c= ].((f2 . p) - r),((f2 . p) + r).[
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in f2 .: W or y in ].((f2 . p) - r),((f2 . p) + r).[ )
assume y in f2 .: W ; :: thesis: y in ].((f2 . p) - r),((f2 . p) + r).[
then consider x being Point of [:(),():] such that
A17: x in W and
A18: f2 . x = y by FUNCT_2:65;
consider x1, x2 being Point of () such that
A19: x = [x1,x2] by BORSUK_1:10;
A20: ( f2 . (x1,x2) = H2(x1,x2) & f2 . (p1,p2) = H2(p1,p2) ) by A8;
x2 in Ball (p2,r) by ;
then A21: |.(x2 - p2).| < r by TOPREAL9:7;
dom (x2 - p2) = Seg n by FINSEQ_1:89;
then (x2 . i) - (p2 . i) = (x2 - p2) . i by VALUED_1:13;
then |.((x2 . i) - (p2 . i)).| <= |.(x2 - p2).| by ;
then |.((f2 . x) - (f2 . p)).| < r by ;
hence y in ].((f2 . p) - r),((f2 . p) + r).[ by ; :: thesis: verum
end;
then f2 is continuous by TOPS_4:21;
then consider g being Function of [:(),():],R^1 such that
A22: for p being Point of [:(),():]
for r1, r2 being Real st f1 . p = r1 & f2 . p = r2 holds
g . p = r1 * r2 and
A23: g is continuous by ;
now :: thesis: for a, b being Point of () holds f . (a,b) = g . (a,b)
let a, b be Point of (); :: thesis: f . (a,b) = g . (a,b)
A24: ( f1 . (a,b) = H1(a,b) & f2 . (a,b) = H2(a,b) ) by A7, A8;
thus f . (a,b) = (a . i) * (b . i) by A6
.= g . [a,b] by
.= g . (a,b) ; :: thesis: verum
end;
hence (proj (((Seg n) --> R^1),i)) * F is continuous by ; :: thesis: verum
end;
then F is continuous by WAYBEL18:6;
hence TIMES n is continuous by ; :: thesis: verum
end;
suppose n is zero ; :: thesis:
end;
end;