per cases ( not n is zero or n is zero ) ;
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;
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 [:(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
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;
deffunc H1( 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) = H1(a,b) from BINOP_1:sch 4();
reconsider f1 = f1 as Function of [:(TOP-REAL n),(TOP-REAL n):],R^1 by A5;
deffunc H2( Element of the carrier of (TOP-REAL n), Element of the carrier of (TOP-REAL n)) -> Element of REAL = In ((c2 . 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) = H2(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).[ )
proof
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) = H1(x1,x2) & f1 . (p1,p2) = H1(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;
then A15: f1 is continuous by TOPS_4:21;
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
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) = H2(x1,x2) & f2 . (p1,p2) = H2(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;
then f2 is continuous by TOPS_4:21;
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)
let a, b be Point of (TOP-REAL n); :: 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 A22, A24
.= g . (a,b) ; :: thesis: verum
end;
hence (proj (((Seg n) --> R^1),i)) * F is continuous by A23, A5, BINOP_1:2; :: thesis: verum
end;
then F is continuous by WAYBEL18:6;
hence TIMES n is continuous by A1, A2, YELLOW12:36; :: thesis: verum
end;
suppose n is zero ; :: thesis: TIMES n is continuous
then n = 0 ;
hence TIMES n is continuous by Th53; :: thesis: verum
end;
end;