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

end;

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

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 (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:22;

hence TIMES n is continuous by A1, A2, YELLOW12:36; :: thesis: verum

end;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:22;

now :: thesis: for i being Element of Seg n holds (proj (((Seg n) --> R^1),i)) * F is continuous

then
F is continuous
by WAYBEL18:6;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 [:(TOP-REAL n),(TOP-REAL n):],R^1 ;

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

A6: for a, b being Point of (TOP-REAL n) holds f . (a,b) = (a . i) * (b . i)_{1}( Element of the carrier of (TOP-REAL n), Element of the carrier of (TOP-REAL n)) -> Element of REAL = In ((n . i),REAL);

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_{1}(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_{2}( Element of the carrier of (TOP-REAL n), Element of the carrier of (TOP-REAL n)) -> Element of REAL = In ((c_{2} . i),REAL);

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_{2}(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 positive Real 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).[ )

for p being Point of [:(TOP-REAL n),(TOP-REAL n):]

for r being positive Real 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).[ )

then consider g being Function of [:(TOP-REAL n),(TOP-REAL n):],R^1 such that

A22: for p being Point of [:(TOP-REAL n),(TOP-REAL n):]

for r1, r2 being Real st f1 . p = r1 & f2 . p = r2 holds

g . p = r1 * r2 and

A23: g is continuous by A15, JGRAPH_2:25;

end;set P = proj (((Seg n) --> R^1),i);

reconsider f = (proj (((Seg n) --> R^1),i)) * F as Function of [:(TOP-REAL n),(TOP-REAL n):],R^1 ;

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

A6: for a, b being Point of (TOP-REAL n) holds f . (a,b) = (a . i) * (b . i)

proof

deffunc H
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:18

.= (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;thus f . (a,b) = (proj (((Seg n) --> R^1),i)) . (F . (a,b)) by A5, BINOP_1:18

.= (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

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

reconsider f1 = f1 as Function of [:(TOP-REAL n),(TOP-REAL n):],R^1 by A5;

deffunc H

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

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

then A15:
f1 is continuous
by TOPS_4:21;
let p be Point of [:(TOP-REAL n),(TOP-REAL n):]; :: thesis: for r being positive Real 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 positive Real; :: 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:10;

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:6;

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:13;

hence p in W by A9, ZFMISC_1:def 2; :: 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 [:(TOP-REAL n),(TOP-REAL n):] such that

A10: x in W and

A11: f1 . x = y by FUNCT_2:65;

consider x1, x2 being Point of (TOP-REAL n) such that

A12: x = [x1,x2] by BORSUK_1:10;

A13: ( f1 . (x1,x2) = H_{1}(x1,x2) & f1 . (p1,p2) = H_{1}(p1,p2) )
by A7;

x1 in Ball (p1,r) by A10, A12, ZFMISC_1:87;

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 A3, REAL_NS1:8;

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

end;( p in W & f1 .: W c= ].((f1 . p) - r),((f1 . p) + r).[ )

let r be positive Real; :: 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:10;

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:6;

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:13;

hence p in W by A9, ZFMISC_1:def 2; :: 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 [:(TOP-REAL n),(TOP-REAL n):] such that

A10: x in W and

A11: f1 . x = y by FUNCT_2:65;

consider x1, x2 being Point of (TOP-REAL n) such that

A12: x = [x1,x2] by BORSUK_1:10;

A13: ( f1 . (x1,x2) = H

x1 in Ball (p1,r) by A10, A12, ZFMISC_1:87;

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 A3, REAL_NS1:8;

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

for p being Point of [:(TOP-REAL n),(TOP-REAL n):]

for r being positive Real 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

then
f2 is continuous
by TOPS_4:21;
let p be Point of [:(TOP-REAL n),(TOP-REAL n):]; :: thesis: for r being positive Real 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 positive Real; :: 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

A16: p = [p1,p2] by BORSUK_1:10;

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:6;

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:13;

hence p in W by A16, ZFMISC_1:def 2; :: 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 [:(TOP-REAL n),(TOP-REAL n):] such that

A17: x in W and

A18: f2 . x = y by FUNCT_2:65;

consider x1, x2 being Point of (TOP-REAL n) such that

A19: x = [x1,x2] by BORSUK_1:10;

A20: ( f2 . (x1,x2) = H_{2}(x1,x2) & f2 . (p1,p2) = H_{2}(p1,p2) )
by A8;

x2 in Ball (p2,r) by A17, A19, ZFMISC_1:87;

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 A3, REAL_NS1:8;

then |.((f2 . x) - (f2 . p)).| < r by A16, A19, A20, A21, XXREAL_0:2;

hence y in ].((f2 . p) - r),((f2 . p) + r).[ by A18, RCOMP_1:1; :: thesis: verum

end;( p in W & f2 .: W c= ].((f2 . p) - r),((f2 . p) + r).[ )

let r be positive Real; :: 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

A16: p = [p1,p2] by BORSUK_1:10;

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:6;

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:13;

hence p in W by A16, ZFMISC_1:def 2; :: 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 [:(TOP-REAL n),(TOP-REAL n):] such that

A17: x in W and

A18: f2 . x = y by FUNCT_2:65;

consider x1, x2 being Point of (TOP-REAL n) such that

A19: x = [x1,x2] by BORSUK_1:10;

A20: ( f2 . (x1,x2) = H

x2 in Ball (p2,r) by A17, A19, ZFMISC_1:87;

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 A3, REAL_NS1:8;

then |.((f2 . x) - (f2 . p)).| < r by A16, A19, A20, A21, XXREAL_0:2;

hence y in ].((f2 . p) - r),((f2 . p) + r).[ by A18, RCOMP_1:1; :: thesis: verum

then consider g being Function of [:(TOP-REAL n),(TOP-REAL n):],R^1 such that

A22: for p being Point of [:(TOP-REAL n),(TOP-REAL n):]

for r1, r2 being Real st f1 . p = r1 & f2 . p = r2 holds

g . p = r1 * r2 and

A23: g is continuous by A15, JGRAPH_2:25;

now :: thesis: for a, b being Point of (TOP-REAL n) holds f . (a,b) = g . (a,b)

hence
(proj (((Seg n) --> R^1),i)) * F is continuous
by A23, A5, BINOP_1:2; :: thesis: verumlet a, b be Point of (TOP-REAL n); :: thesis: f . (a,b) = g . (a,b)

A24: ( f1 . (a,b) = H_{1}(a,b) & f2 . (a,b) = H_{2}(a,b) )
by A7, A8;

thus f . (a,b) = (a . i) * (b . i) by A6

.= g . [a,b] by A22, A24

.= g . (a,b) ; :: thesis: verum

end;A24: ( f1 . (a,b) = H

thus f . (a,b) = (a . i) * (b . i) by A6

.= g . [a,b] by A22, A24

.= g . (a,b) ; :: thesis: verum

hence TIMES n is continuous by A1, A2, YELLOW12:36; :: thesis: verum