per cases ( not n is empty or n is empty ) ;

suppose not n is empty ; :: thesis: TIMES n is continuous

then reconsider n = n as non zero Element of NAT by ORDINAL1:def 13;
set T = TOP-REAL n;
set F = TIMES n;
set J = (Seg n) --> R^1 ;
set c = the carrier of (TOP-REAL n);
A1: TopSpaceMetr (Euclid n) = product ((Seg n) --> R^1 ) by EUCLID_9:28;
A2: TopStruct(# the carrier of (TOP-REAL n),the topology of (TOP-REAL n) #) = TopSpaceMetr (Euclid n) by EUCLID:def 8;
then reconsider F = TIMES n as Function of [:(TOP-REAL n),(TOP-REAL n):],(product ((Seg n) --> R^1 )) by EUCLID_9:28;
A3: the carrier of (TOP-REAL n) = REAL n by EUCLID:25;

now

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;
A4: ((Seg n) --> R^1 ) . i = R^1 by FUNCOP_1:13;
reconsider f = (proj ((Seg n) --> R^1 ),i) * F as Function of [:(TOP-REAL n),(TOP-REAL n):],R^1 by FUNCOP_1:13;
A5: the carrier of [:(TOP-REAL n),(TOP-REAL n):] = [:the carrier of (TOP-REAL n),the carrier of (TOP-REAL n):] by BORSUK_1:def 5;
A6: for a, b being Point of (TOP-REAL n) holds f . a,b = (a . i) * (b . i)

proof

let a, b be Point of (TOP-REAL n); :: thesis: f . a,b = (a . i) * (b . i)
thus f . a,b = (proj ((Seg n) --> R^1 ),i) . (F . a,b) by A5, BINOP_1:30
.= (proj ((Seg n) --> R^1 ),i) . (a (#) b) by Def5
.= (a (#) b) . i by A1, A2, YELLOW17:8
.= (a . i) * (b . i) by VALUED_1:5 ; :: thesis: verum

end;

deffunc H₁( Element of the carrier of (TOP-REAL n), Element of the carrier of (TOP-REAL n)) -> Element of REAL = n . i;
consider f1 being Function of [:the carrier of (TOP-REAL n),the carrier of (TOP-REAL n):],REAL such that
A7: for a, b being Element of the carrier of (TOP-REAL n) holds f1 . a,b = H₁(a,b) from BINOP_1:sch 4();
reconsider f1 = f1 as Function of [:(TOP-REAL n),(TOP-REAL n):],R^1 by A5;
deffunc H₂( Element of the carrier of (TOP-REAL n), Element of the carrier of (TOP-REAL n)) -> Element of REAL = c₂ . i;
consider f2 being Function of [:the carrier of (TOP-REAL n),the carrier of (TOP-REAL n):],REAL such that
A8: for a, b being Element of the carrier of (TOP-REAL n) holds f2 . a,b = H₂(a,b) from BINOP_1:sch 4();
reconsider f1 = f1, f2 = f2 as Function of [:(TOP-REAL n),(TOP-REAL n):],R^1 by A5;
for p being Point of [:(TOP-REAL n),(TOP-REAL n):]
for r being real positive number ex W being open Subset of [:(TOP-REAL n),(TOP-REAL n):] st
( p in W & f1 .: W c= ].((f1 . p) - r),((f1 . p) + r).[ )

proof

let p be Point of [:(TOP-REAL n),(TOP-REAL n):]; :: thesis: for r being real positive number ex W being open Subset of [:(TOP-REAL n),(TOP-REAL n):] st
( p in W & f1 .: W c= ].((f1 . p) - r),((f1 . p) + r).[ )
let r be real positive number ; :: thesis: ex W being open Subset of [:(TOP-REAL n),(TOP-REAL n):] st
( p in W & f1 .: W c= ].((f1 . p) - r),((f1 . p) + r).[ )
consider p1, p2 being Point of (TOP-REAL n) such that
A9: p = [p1,p2] by BORSUK_1:50;
set B1 = Ball p1,r;
set B2 = [#] (TOP-REAL n);
reconsider W = [:(Ball p1,r),([#] (TOP-REAL n)):] as open Subset of [:(TOP-REAL n),(TOP-REAL n):] by BORSUK_1:46;
take W ; :: thesis: ( p in W & f1 .: W c= ].((f1 . p) - r),((f1 . p) + r).[ )
( p1 in Ball p1,r & p2 in [#] (TOP-REAL n) ) by TOPGEN_5:17;
hence p in W by A9, ZFMISC_1:def 2; :: thesis: f1 .: W c= ].((f1 . p) - r),((f1 . p) + r).[
let y be set ; :: 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 [:(TOP-REAL n),(TOP-REAL n):] such that
A10: x in W and
A11: f1 . x = y by FUNCT_2:116;
consider x1, x2 being Point of (TOP-REAL n) such that
A12: x = [x1,x2] by BORSUK_1:50;
A13: ( f1 . x1,x2 = x1 . i & f1 . p1,p2 = p1 . i ) by A7;
x1 in Ball p1,r by A10, A12, ZFMISC_1:106;
then A14: |.(x1 - p1).| < r by TOPREAL9:7;
dom (x1 - p1) = Seg n by EUCLID:3;
then (x1 . i) - (p1 . i) = (x1 - p1) . i by VALUED_1:13;
then abs ((x1 . i) - (p1 . i)) <= |.(x1 - p1).| by A3, REAL_NS1:8;
then abs ((f1 . x) - (f1 . p)) < r by A9, A12, A13, A14, XXREAL_0:2;
hence y in ].((f1 . p) - r),((f1 . p) + r).[ by A11, RCOMP_1:8; :: thesis: verum

end;

then A16: f1 is continuous by TOPS_4:21;
for p being Point of [:(TOP-REAL n),(TOP-REAL n):]
for r being real positive number ex W being open Subset of [:(TOP-REAL n),(TOP-REAL n):] st
( p in W & f2 .: W c= ].((f2 . p) - r),((f2 . p) + r).[ )

proof

let p be Point of [:(TOP-REAL n),(TOP-REAL n):]; :: thesis: for r being real positive number ex W being open Subset of [:(TOP-REAL n),(TOP-REAL n):] st
( p in W & f2 .: W c= ].((f2 . p) - r),((f2 . p) + r).[ )
let r be real positive number ; :: thesis: ex W being open Subset of [:(TOP-REAL n),(TOP-REAL n):] st
( p in W & f2 .: W c= ].((f2 . p) - r),((f2 . p) + r).[ )
consider p1, p2 being Point of (TOP-REAL n) such that
A17: p = [p1,p2] by BORSUK_1:50;
set B1 = [#] (TOP-REAL n);
set B2 = Ball p2,r;
reconsider W = [:([#] (TOP-REAL n)),(Ball p2,r):] as open Subset of [:(TOP-REAL n),(TOP-REAL n):] by BORSUK_1:46;
take W ; :: thesis: ( p in W & f2 .: W c= ].((f2 . p) - r),((f2 . p) + r).[ )
( p1 in [#] (TOP-REAL n) & p2 in Ball p2,r ) by TOPGEN_5:17;
hence p in W by A17, ZFMISC_1:def 2; :: thesis: f2 .: W c= ].((f2 . p) - r),((f2 . p) + r).[
let y be set ; :: 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 [:(TOP-REAL n),(TOP-REAL n):] such that
A18: x in W and
A19: f2 . x = y by FUNCT_2:116;
consider x1, x2 being Point of (TOP-REAL n) such that
A20: x = [x1,x2] by BORSUK_1:50;
A21: ( f2 . x1,x2 = x2 . i & f2 . p1,p2 = p2 . i ) by A8;
x2 in Ball p2,r by A18, A20, ZFMISC_1:106;
then A22: |.(x2 - p2).| < r by TOPREAL9:7;
dom (x2 - p2) = Seg n by EUCLID:3;
then (x2 . i) - (p2 . i) = (x2 - p2) . i by VALUED_1:13;
then abs ((x2 . i) - (p2 . i)) <= |.(x2 - p2).| by A3, REAL_NS1:8;
then abs ((f2 . x) - (f2 . p)) < r by A17, A20, A21, A22, XXREAL_0:2;
hence y in ].((f2 . p) - r),((f2 . p) + r).[ by A19, RCOMP_1:8; :: thesis: verum

end;

then f2 is continuous by TOPS_4:21;
then consider g being Function of [:(TOP-REAL n),(TOP-REAL n):],R^1 such that
A24: for p being Point of [:(TOP-REAL n),(TOP-REAL n):]
for r1, r2 being real number st f1 . p = r1 & f2 . p = r2 holds
g . p = r1 * r2 and
A25: g is continuous by A16, JGRAPH_2:35;

now

let a, b be Point of (TOP-REAL n); :: thesis: f . a,b = g . a,b
A26: ( f1 . a,b = a . i & f2 . a,b = b . i ) by A7, A8;
thus f . a,b = (a . i) * (b . i) by A6
.= g . [a,b] by A24, A26
.= g . a,b ; :: thesis: verum

end;

hence (proj ((Seg n) --> R^1 ),i) * F is continuous by A25, A4, A5, BINOP_1:2; :: thesis: verum

end;

then F is continuous by WAYBEL18:7;
hence TIMES n is continuous by A1, A2, YELLOW12:36; :: thesis: verum

end;

suppose n is empty ; :: thesis: TIMES n is continuous

hence TIMES n is continuous by Th53; :: thesis: verum

end;

end;