:: On the Continuity of Some Functions :: by Artur Korni{\l}owicz :: :: Received February 9, 2010 :: Copyright (c) 2010 Association of Mizar Users environ vocabularies RELAT_1, FUNCT_1, VALUED_0, TOPS_1, MEMBERED, XBOOLE_0, ARYTM_1, COMPLEX1, ARYTM_3, XCMPLX_0, FINSEQ_1, EUCLID, PRE_TOPC, ORDINAL2, TOPREALB, METRIC_1, XREAL_0, TOPMETR, RCOMP_1, PCOMPS_1, FUNCT_3, FINSEQ_2, RLVECT_1, RVSUM_1, SQUARE_1, FUNCT_4, VALUED_2, ALGSTR_0, SUBSET_1, FUNCOP_1, PARTFUN1, CARD_3, FINSET_1, ZFMISC_1, TARSKI, CARD_1, TOPREALC, NAT_1, ORDINAL1, XXREAL_0, VALUED_1, NUMBERS, ORDINAL4, STRUCT_0, XXREAL_1, SUPINF_2; notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, FINSET_1, RELAT_1, FUNCT_1, RELSET_1, PARTFUN1, FUNCT_2, BINOP_1, ORDINAL1, NUMBERS, VALUED_0, VALUED_1, CARD_1, XCMPLX_0, XREAL_0, XXREAL_0, FUNCT_3, MEMBERED, COMPLEX1, SQUARE_1, NAT_1, FUNCOP_1, FINSEQ_1, FINSEQ_2, RCOMP_1, FUNCT_7, VALUED_2, STRUCT_0, RVSUM_1, PRE_TOPC, TOPS_1, METRIC_1, PCOMPS_1, TOPMETR, T_0TOPSP, BORSUK_1, ALGSTR_0, RLVECT_1, RLTOPSP1, EUCLID, WAYBEL18, TOPREAL9, TOPREALB; constructors SEQ_1, MONOID_0, FUNCT_7, FINSEQOP, VALUED_2, TOPREAL9, TOPREALB, TOPS_1, BORSUK_4, COMPLEX1, T_0TOPSP, SQUARE_1, TSP_1, FUNCT_4, FUNCSDOM, CONVEX1, WAYBEL18, SETFAM_1, BINOP_2, EUCLID_7, EUCLID_9; registrations XBOOLE_0, RELAT_1, FUNCT_1, VALUED_0, VALUED_1, MEMBERED, XCMPLX_0, XREAL_0, VALUED_2, PRE_TOPC, STRUCT_0, EUCLID, MONOID_0, TOPREALB, XXREAL_0, NAT_1, BORSUK_4, BORSUK_6, TOPMETR, FUNCT_2, RVSUM_1, TOPREAL9, SQUARE_1, RCOMP_1, TOPS_1, FUNCT_7, NUMBERS, RLVECT_1, FINSEQ_1, FUNCOP_1, WAYBEL18, BORSUK_1, PRE_POLY, JORDAN2B, ZFMISC_1, FINSEQ_2, REALSET1, ORDINAL1, PARTFUN3, EUCLID_9; requirements SUBSET, BOOLE, NUMERALS, ARITHM, REAL; definitions FINSEQ_1, RLVECT_1, TARSKI, XBOOLE_0, LATTICE7, FUNCT_1, FUNCT_2, XCMPLX_0, SQUARE_1, BINOP_1, FUNCOP_1, VALUED_0, VALUED_1, FINSEQ_2, VALUED_2, STRUCT_0, METRIC_1, PCOMPS_1, TOPMETR, CONVEX1, RLTOPSP1, EUCLID, BORSUK_4, TOPREALB, RVSUM_1, EUCLID_9; theorems FUNCT_1, PARTFUN1, FUNCT_2, VALUED_1, FUNCT_7, SEQ_2, VALUED_2, BORSUK_1, TOPREALB, TOPMETR, TOPREAL9, EUCLID, JGRAPH_2, JGRAPH_6, GOBOARD6, TOPS_1, METRIC_1, JGRAPH_1, TOPRNS_1, XXREAL_0, XREAL_1, XBOOLE_0, RCOMP_1, JORDAN2B, FINSEQ_2, XREAL_0, FINSEQ_1, NAT_1, FUNCOP_1, PRE_TOPC, SQUARE_1, TOPREAL6, RVSUM_1, COMPLEX1, XXREAL_1, RELAT_1, XCMPLX_1, ORDINAL1, TSP_1, RLVECT_1, TOPS_3, YELLOW12, JORDAN2C, TOPGEN_5, YELLOW17, ZFMISC_1, REAL_NS1, WAYBEL18, BINOP_1, JGRAPH_4, SUBSET_1, ABSVALUE, CARD_1, REALSET1, STRUCT_0, PRVECT_2, TOPREAL7, EUCLID_9, TOPS_4; schemes FUNCT_2, BINOP_1, FINSEQ_2; begin :: Preliminaries reserve x, X for set, i, n, m for Nat, r, s for real number, c, c1, c2, d for complex number, f, g for complex-valued Function, g1 for n-long complex-valued FinSequence, f1 for n-long real-valued FinSequence, T for non empty TopSpace, p for Element of TOP-REAL n; registration let R be Relation, X be empty set; cluster R.:X -> empty; coherence by RELAT_1:149; cluster R"X -> empty; coherence by RELAT_1:171; end; registration let A be empty set; cluster -> empty Element of A; coherence by SUBSET_1:def 2; end; theorem for X being trivial set, Y being set st X,Y are_equipotent holds Y is trivial proof let X be trivial set, Y be set such that A1: X,Y are_equipotent; A2: card X < 2 by REALSET1:13; A3: Y is finite by A1,CARD_1:68; card X = card Y by A1,CARD_1:21; hence thesis by A2,A3,REALSET1:13; end; registration let r be real number; cluster r^2 -> non negative; coherence; end; registration let r be positive (real number); cluster r^2 -> positive; coherence; end; registration cluster sqrt(0) -> zero; coherence by SQUARE_1:82; end; registration let f be empty set; cluster sqr(f) -> empty; coherence; cluster |.f.| -> zero; coherence by RVSUM_1:102; end; theorem Th2: f(#)(c1+c2) = f(#)c1 + f(#)c2 proof A1: dom (f(#)(c1+c2)) = dom f by VALUED_1:def 5; A2: dom (f(#)c1) = dom f by VALUED_1:def 5; A3: dom (f(#)c2) = dom f by VALUED_1:def 5; A4: dom (f(#)c1 + f(#)c2) = dom (f(#)c1) /\ dom (f(#)c2) by VALUED_1:def 1; hence dom (f(#)(c1+c2)) = dom (f(#)c1 + f(#)c2) by A2,A3,VALUED_1:def 5; let x; assume A5: x in dom (f(#)(c1+c2)); hence (f(#)(c1+c2)).x = f.x * (c1+c2) by VALUED_1:def 5 .= f.x*c1 + f.x*c2 .= (f(#)c1).x + f.x*c2 by A1,A2,A5,VALUED_1:def 5 .= (f(#)c1).x + (f(#)c2).x by A1,A3,A5,VALUED_1:def 5 .= (f(#)c1 + f(#)c2).x by A1,A2,A3,A4,A5,VALUED_1:def 1; end; theorem f(#)(c1-c2) = f(#)c1 - f(#)c2 proof thus f(#)(c1-c2) = f(#)c1 + f(#)-c2 by Th2 .= f(#)c1 - f(#)c2 by VALUED_2:24; end; theorem Th4: f(/)c + g(/)c = (f+g)(/)c proof A1: dom (f(/)c + g(/)c) = dom (f(/)c) /\ dom (g(/)c) by VALUED_1:def 1; A2: dom (f(/)c) = dom f by VALUED_2:28; A3: dom (g(/)c) = dom g by VALUED_2:28; A4: dom ((f+g)(/)c) = dom (f+g) by VALUED_2:28; A5: dom (f+g) = dom f /\ dom g by VALUED_1:def 1; thus dom (f(/)c + g(/)c) = dom ((f+g)(/)c) by A1,A2,A3,A4,VALUED_1:def 1; let x; assume A6: x in dom (f(/)c + g(/)c); thus ((f+g)(/)c).x = (f+g).x/c by VALUED_2:29 .= (f.x+g.x)/c by A1,A2,A3,A6,A5,VALUED_1:def 1 .= f.x/c + g.x/c .= f.x/c + (g(/)c).x by VALUED_2:29 .= (f(/)c).x + (g(/)c).x by VALUED_2:29 .= (f(/)c + g(/)c).x by A6,VALUED_1:def 1; end; theorem f(/)c - g(/)c = (f-g)(/)c proof thus f(/)c - g(/)c = f(/)c + (-g)(/)c by VALUED_2:30 .= (f-g)(/)c by Th4; end; theorem c1 <> 0 & c2 <> 0 implies f(/)c1 - g(/)c2 = (f(#)c2-g(#)c1) (/) (c1*c2) proof assume A1: c1 <> 0 & c2 <> 0; A2: dom (f(/)c1) = dom f by VALUED_2:28; A3: dom (g(/)c2) = dom g by VALUED_2:28; A4: dom (f(#)c2) = dom f by VALUED_1:def 5; A5: dom (g(#)c1) = dom g by VALUED_1:def 5; A6: dom (f(/)c1-g(/)c2) = dom (f(/)c1) /\ dom (g(/)c2) by VALUED_1:12; A7: dom (f(#)c2-g(#)c1) = dom (f(#)c2) /\ dom (g(#)c1) by VALUED_1:12; hence dom (f(/)c1 - g(/)c2) = dom ((f(#)c2-g(#)c1) (/) (c1*c2)) by A2,A3,A4,A5,A6,VALUED_2:28; let x; assume A8: x in dom (f(/)c1 - g(/)c2); hence ((f(/)c1 - g(/)c2)).x = (f(/)c1).x - (g(/)c2).x by VALUED_1:13 .= (f.x/c1) - (g(/)c2).x by VALUED_2:29 .= (f.x/c1) - (g.x/c2) by VALUED_2:29 .= (f.x*c2-g.x*c1) / (c1*c2) by A1,XCMPLX_1:131 .= (f.x*c2-(g(#)c1).x) / (c1*c2) by VALUED_1:6 .= ((f(#)c2).x-(g(#)c1).x) / (c1*c2) by VALUED_1:6 .= ((f(#)c2-g(#)c1)).x / (c1*c2) by A2,A3,A4,A5,A6,A7,A8,VALUED_1:13 .= ((f(#)c2-g(#)c1) (/) (c1*c2)).x by VALUED_2:29; end; theorem c <> 0 implies f(/)c - g = (f-c(#)g) (/) c proof assume A1: c <> 0; A2: dom(f(/)c - g) = dom(f(/)c) /\ dom g by VALUED_1:12 .= dom f /\ dom g by VALUED_2:28; A3: dom(f-c(#)g) = dom f /\ dom(c(#)g) by VALUED_1:12 .= dom f /\ dom g by VALUED_1:def 5; hence dom(f(/)c - g) = dom((f-c(#)g) (/) c) by A2,VALUED_2:28; let x be set; assume A4: x in dom(f(/)c - g); hence (f(/)c - g).x = (f(/)c).x - g.x by VALUED_1:13 .= f.x/c - g.x by VALUED_2:29 .= f.x/c - c*g.x/c by A1,XCMPLX_1:90 .= f.x/c - (c(#)g).x/c by VALUED_1:6 .= (f.x-(c(#)g).x) / c .= ((f-c(#)g)).x / c by A2,A3,A4,VALUED_1:13 .= ((f-c(#)g) (/) c).x by VALUED_2:29; end; theorem (c-d)(#)f = c(#)f - d(#)f proof dom(c(#)f - d(#)f) = dom(c(#)f) /\ dom(d(#)f) by VALUED_1:12 .= dom f /\ dom(d(#)f) by VALUED_1:def 5 .= dom f /\ dom f by VALUED_1:def 5; hence A1: dom((c-d)(#)f) = dom(c(#)f - d(#)f) by VALUED_1:def 5; let x be set; assume A2: x in dom((c-d)(#)f); thus ((c-d)(#)f).x = (c-d)*f.x by VALUED_1:6 .= c*f.x - d*f.x .= c*f.x - (d(#)f).x by VALUED_1:6 .= (c(#)f).x - (d(#)f).x by VALUED_1:6 .= (c(#)f - d(#)f).x by A1,A2,VALUED_1:13; end; theorem (f-g)^2 = (g-f)^2 proof A1: dom(f-g) = dom f /\ dom g by VALUED_1:12; A2: dom(g-f) = dom g /\ dom f by VALUED_1:12; A3: dom((f-g)^2) = dom(f-g) by VALUED_1:11; hence dom((f-g)^2) = dom((g-f)^2) by A1,A2,VALUED_1:11; let x be set; assume A4: x in dom((f-g)^2); then A5: (f-g).x = f.x - g.x by A3,VALUED_1:13; A6: (g-f).x = g.x - f.x by A1,A3,A4,A2,VALUED_1:13; thus ((f-g)^2).x = (f-g).x * (f-g).x by VALUED_1:5 .= (g-f).x * (g-f).x by A5,A6 .= ((g-f)^2).x by VALUED_1:5; end; theorem (f(/)c)^2 = f^2 (/) c^2 proof thus dom((f(/)c)^2) = dom(f(/)c) by VALUED_1:11 .= dom f by VALUED_2:28 .= dom(f^2) by VALUED_1:11 .= dom(f^2 (/) c^2) by VALUED_2:28; let x be set; assume x in dom((f(/)c)^2); thus ((f(/)c)^2).x = ((f(/)c).x)^2 by VALUED_1:11 .= (f.x/c)^2 by VALUED_2:29 .= (f.x)^2 / c^2 by XCMPLX_1:77 .= (f^2).x / c^2 by VALUED_1:11 .= (f^2 (/) c^2).x by VALUED_2:29; end; theorem Th11: |. (n|->r) - (n|->s) .| = sqrt(n) * abs(r-s) proof thus |. (n|->r) - (n|->s) .| = sqrt Sum sqr (n|->(r-s)) by RVSUM_1:51 .= sqrt Sum (n|->(r-s)^2) by RVSUM_1:82 .= sqrt (n*(r-s)^2) by RVSUM_1:110 .= sqrt n * sqrt((r-s)^2) by SQUARE_1:97 .= sqrt n * abs(r-s) by COMPLEX1:158; end; registration let f,x,c; cluster f+*(x,c) -> complex-valued; coherence proof set F = f+*(x,c); let a be set such that a in dom F; per cases; suppose x in dom f & x = a; hence thesis by FUNCT_7:33; end; suppose x in dom f & x <> a; then F.a = f.a by FUNCT_7:34; hence thesis; end; suppose not x in dom f; then F.a = f.a by FUNCT_7:def 3; hence thesis; end; end; end; theorem Th12: ((0*n)+*(x,c))^2 = (0*n)+*(x,c^2) proof set f = (0*n)+*(x,c); set g = (0*n)+*(x,c^2); A1: dom f = dom (0*n) by FUNCT_7:32; A2: dom g = dom (0*n) by FUNCT_7:32; A3: dom (f^2) = dom f by VALUED_1:11; thus dom (f^2) = dom g by A1,A2,VALUED_1:11; let a be set; assume A4: a in dom (f^2); A5: (f^2).a = (f.a)^2 by VALUED_1:11; per cases; suppose A6: a = x; then f.a = c by A1,A3,A4,FUNCT_7:33; hence thesis by A6,A1,A3,A4,A5,FUNCT_7:33; end; suppose A7: a <> x; then A8: f.a = (n|->0).a by FUNCT_7:34 .= {}.x; g.a = (n|->0).a by A7,FUNCT_7:34 .= {}.x; hence thesis by A5,A8; end; end; theorem Th13: x in Seg n implies |.(0*n)+*(x,r).| = abs(r) proof set f = (0*n)+*(x,r); A1: r^2 in REAL by XREAL_0:def 1; A2: n in NAT by ORDINAL1:def 13; assume A3: x in Seg n; f^2 = (0*n)+*(x,r^2) by Th12; then Sum (f^2) = r^2 by A3,A1,A2,JORDAN2B:14; hence thesis by COMPLEX1:158; end; theorem Th14: (0.REAL n)+*(x,0) = 0.REAL n proof set p = (0.REAL n)+*(x,0); A1: dom p = Seg n by EUCLID:3; A2: dom ((0.REAL n)+*(x,0)) = dom (0.REAL n) by FUNCT_7:32; A3: dom (0.REAL n) = Seg n by EUCLID:3; now let z be set; assume A4: z in dom p; per cases; suppose z = x; hence p.z = 0 by A1,A3,A4,FUNCT_7:33 .= (0.REAL n).z; end; suppose z <> x; hence p.z = (0.REAL n).z by FUNCT_7:34; end; end; hence thesis by A2,FUNCT_1:9; end; theorem Th15: mlt(f1,(0.REAL n)+*(x,r)) = (0.REAL n)+*(x,f1.x*r) proof set p = (0.REAL n)+*(x,r); A1: dom f1 = Seg n by EUCLID:3; A2: dom p = Seg n by EUCLID:3; A3: dom mlt(f1,p) = dom f1 /\ dom p by VALUED_1:def 4; A4: dom ((0.REAL n)+*(x,f1.x*r)) = dom (0.REAL n) by FUNCT_7:32; A5: dom (0.REAL n) = Seg n by EUCLID:3; now let z be set; assume A6: z in dom mlt(f1,p); A7: (mlt(f1,p)).z = f1.z*p.z by VALUED_1:5; per cases; suppose A8: z = x; hence (mlt(f1,p)).z = f1.z*r by A1,A2,A3,A5,A6,A7,FUNCT_7:33 .= ((0.REAL n)+*(x,f1.x*r)).z by A1,A2,A3,A5,A6,A8,FUNCT_7:33; end; suppose A9: z <> x; hence (mlt(f1,p)).z = f1.z*(0.REAL n).z by A7,FUNCT_7:34 .= f1.z*(n|->0).z .= ((0.REAL n)+*(x,f1.x*r)).z by A9,FUNCT_7:34; end; end; hence thesis by A4,A5,EUCLID:3,FUNCT_1:9; end; theorem |(f1,(0.REAL n)+*(x,r))| = f1.x * r proof A1: mlt(f1,(0.REAL n)+*(x,r)) = (0.REAL n)+*(x,f1.x*r) by Th15; A2: dom f1 = Seg n by EUCLID:3; A3: n in NAT by ORDINAL1:def 13; A4: f1.x*r in REAL by XREAL_0:def 1; per cases; suppose x in dom f1; hence thesis by A1,A2,A3,A4,JORDAN2B:14; end; suppose not x in dom f1; then A5: f1.x = 0 by FUNCT_1:def 4; hence |(f1,(0.REAL n)+*(x,r))| = Sum 0.REAL n by A1,Th14 .= f1.x * r by A5,A3,JORDAN2B:11; end; end; theorem Th17: (g1+*(i,c)) - g1 = (0*n)+*(i,c-(g1.i)) proof A1: dom (g1+*(i,c) - g1) = dom (g1+*(i,c)) /\ dom g1 by VALUED_1:12; A2: dom (0*n) = Seg n by EUCLID:3; A3: dom g1 = Seg n by EUCLID:3; A4: dom (g1+*(i,c)) = dom g1 by FUNCT_7:32; hence dom (g1+*(i,c) - g1) = dom ((0*n)+*(i,c-(g1.i))) by A1,A3,EUCLID:3; let x; assume A5: x in dom (g1+*(i,c) - g1); then A6: (g1+*(i,c) - g1).x = (g1+*(i,c)).x - g1.x by VALUED_1:13; per cases; suppose A7: x = i; hence (g1+*(i,c) - g1).x = c - g1.x by A6,A1,A5,A4,FUNCT_7:33 .= ((0*n)+*(i,c-(g1.i))).x by A1,A2,A3,A5,A4,A7,FUNCT_7:33; end; suppose A8: x <> i; hence (g1+*(i,c) - g1).x = g1.x - g1.x by A6,FUNCT_7:34 .= (n|->0).x .= ((0*n)+*(i,c-(g1.i))).x by A8,FUNCT_7:34; end; end; theorem |.<*r*>.| = abs(r) proof set f = <*r*>; sqr f = <*r^2*> by RVSUM_1:81; then Sum sqr f = r^2 by RVSUM_1:103; hence thesis by COMPLEX1:158; end; theorem Th19: for f being real-valued FinSequence holds f is FinSequence of REAL proof let f be real-valued FinSequence; rng f c= REAL; hence thesis by FINSEQ_1:def 4; end; theorem for f being real-valued FinSequence st |.f.| <> 0 ex i being Nat st i in dom f & f.i <> 0 proof let f be real-valued FinSequence; assume |.f.| <> 0; then consider i being Element of NAT such that A1: i in dom sqr f and A2: (sqr f).i <> 0 by PRVECT_2:3,SQUARE_1:82; take i; thus i in dom f by A1,VALUED_1:11; (sqr f).i = (f.i)^2 by VALUED_1:11; hence thesis by A2; end; theorem Th21: for f being real-valued FinSequence holds abs Sum f <= Sum abs f proof let f be real-valued FinSequence; defpred P[set] means ex F being real-valued FinSequence st F = $1 & abs Sum F <= Sum abs F; A1: P[<*>REAL] proof take <*>REAL; thus thesis by ABSVALUE:7,RVSUM_1:102; end; A2: for p being FinSequence of REAL, x being Element of REAL st P[p] holds P[p^<*x*>] proof let p be FinSequence of REAL, x be Element of REAL; given F being real-valued FinSequence such that A3: F = p and A4: abs Sum F <= Sum abs F; A5: abs Sum F + abs x <= Sum abs F + abs x by A4,XREAL_1:8; take G = p^<*x*>; A6: abs <*x*> = <*abs(x)*> by JORDAN2B:23; A7: Sum <*abs(x)*> = abs(x) by RVSUM_1:103; abs G = (abs p)^abs<*x*> by TOPREAL7:12; then A8: Sum abs G = Sum abs p + abs x by A6,A7,RVSUM_1:105; Sum G = Sum p + x by RVSUM_1:104; then abs Sum G <= abs Sum p + abs x by COMPLEX1:142; hence thesis by A8,A3,A5,XXREAL_0:2; end; A9: for p being FinSequence of REAL holds P[p] from FINSEQ_2:sch 2(A1,A2); f is FinSequence of REAL by Th19; then P[f] by A9; hence thesis; end; Lm1: for f being n-long real-valued FinSequence holds f is Element of n-tuples_on REAL proof let f be n-long real-valued FinSequence; A1: f is FinSequence of REAL by Th19; len f = n by FINSEQ_1:def 18; hence thesis by A1,FINSEQ_2:110; end; theorem for A being non empty 1-sorted, B being trivial non empty 1-sorted for t being Point of B for f being Function of A,B holds f = A --> t proof let A be non empty 1-sorted; let B be trivial non empty 1-sorted; let t be Point of B; let f be Function of A,B; let a be Element of A; thus f.a = (A --> t).a by STRUCT_0:def 10; end; registration let n be non zero Nat, i be Element of Seg n; let T be real-membered non empty TopSpace; cluster proj(Seg n --> T,i) -> real-valued; coherence proof (Seg n --> T).i = T by FUNCOP_1:13; hence thesis; end; end; definition let n; let p be Element of REAL n; let r; redefine func p(/)r -> Element of REAL n; coherence proof A1: p(/)r is FinSequence of REAL by Th19; A2: len p = n by FINSEQ_1:def 18; Seg len (p(/)r) = dom (p(/)r) by FINSEQ_1:def 3 .= dom p by VALUED_1:def 5 .= Seg n by A2,FINSEQ_1:def 3; then len (p(/)r) = n by FINSEQ_1:8; hence thesis by A1,FINSEQ_2:110; end; end; theorem Th23: for p, q being Point of TOP-REAL m holds p in Ball(q,r) iff -p in Ball(-q,r) proof let p, q be Point of TOP-REAL m; A1: m in NAT by ORDINAL1:def 13; A2: now let a, b be Point of TOP-REAL m; assume a in Ball(b,r); then A3: |.a-b.| < r by A1,TOPREAL9:7; -a--b = (-a)+-(-b) .= -(a-b) by RLVECT_1:45; then |.-a--b.| = |.a-b.| by EUCLID:75; hence -a in Ball(-b,r) by A1,A3,TOPREAL9:7; end; --p = p & --q = q; hence thesis by A2; end; definition let S be 1-sorted; attr S is complex-functions-membered means :Def1: the carrier of S is complex-functions-membered; attr S is real-functions-membered means :Def2: the carrier of S is real-functions-membered; end; registration let n; cluster TOP-REAL n -> real-functions-membered; coherence proof let x; assume x in the carrier of TOP-REAL n; then reconsider x as Point of TOP-REAL n; x is real-valued; hence thesis; end; end; registration cluster TOP-REAL 0 -> real-membered; coherence proof thus the carrier of TOP-REAL 0 is real-membered by EUCLID:25,JORDAN2C:113; end; end; registration cluster TOP-REAL 0 -> trivial; coherence by EUCLID:25,JORDAN2C:113; end; registration cluster real-functions-membered -> complex-functions-membered 1-sorted; coherence proof let S be 1-sorted; assume A1: the carrier of S is real-functions-membered; let x; thus thesis by A1; end; end; registration cluster strict non empty real-functions-membered 1-sorted; existence proof take S = 1-sorted(#{the real-valued Function}#); thus S is strict; thus the carrier of S is non empty; let x; thus thesis; end; end; registration let S be complex-functions-membered 1-sorted; cluster the carrier of S -> complex-functions-membered; coherence by Def1; end; registration let S be real-functions-membered 1-sorted; cluster the carrier of S -> real-functions-membered; coherence by Def2; end; registration cluster strict non empty real-functions-membered TopSpace; existence proof take the TopStruct of TOP-REAL 1; thus thesis by Def2; end; end; registration let S be complex-functions-membered TopSpace; cluster -> complex-functions-membered SubSpace of S; coherence proof let A be SubSpace of S; let x; the carrier of A c= the carrier of S by BORSUK_1:35; hence thesis; end; end; registration let S be real-functions-membered TopSpace; cluster -> real-functions-membered SubSpace of S; coherence proof let A be SubSpace of S; let x; the carrier of A c= the carrier of S by BORSUK_1:35; hence thesis; end; end; definition let X be complex-functions-membered set; func (-)X -> complex-functions-membered set means :Def3: for f being complex-valued Function holds -f in it iff f in X; existence proof set F = {-f where f is Element of X: f in X}; F is complex-functions-membered proof let x; assume x in F; then ex f being Element of X st x = -f & f in X; hence thesis; end; then reconsider F as complex-functions-membered set; take F; let f be complex-valued Function; hereby assume -f in F; then ex g being Element of X st -f = -g & g in X; hence f in X by RVSUM_1:43; end; thus thesis; end; uniqueness proof let A, B be complex-functions-membered set such that A1: for f being complex-valued Function holds -f in A iff f in X and A2: for f being complex-valued Function holds -f in B iff f in X; thus A c= B proof let x; assume A3: x in A; then reconsider x as Element of A; A4: --x = x; then -x in X by A1,A3; hence thesis by A2,A4; end; let x; assume A5: x in B; then reconsider x as Element of B; A6: --x = x; then -x in X by A2,A5; hence thesis by A1,A6; end; involutiveness proof let r, A be complex-functions-membered set; assume A7: for f being complex-valued Function holds -f in r iff f in A; let f be complex-valued Function; hereby assume -f in A; then --f in r by A7; hence f in r; end; assume f in r; then --f in r; hence -f in A by A7; end; end; registration let X be empty set; cluster (-)X -> empty; coherence proof assume not thesis; then consider x being set such that A1: x in (-)X by XBOOLE_0:def 1; reconsider x as Element of (-)X by A1; --x = x; hence thesis by A1,Def3; end; end; registration let X be non empty complex-functions-membered set; cluster (-)X -> non empty; coherence proof consider x being set such that A1: x in X by XBOOLE_0:def 1; reconsider x as Element of X by A1; -x in (-)X by Def3; hence thesis; end; end; theorem Th24: for X being complex-functions-membered set, f being complex-valued Function holds -f in X iff f in (-)X proof let X be complex-functions-membered set, f be complex-valued Function; --f = f & (-)(-)X = X; hence thesis by Def3; end; registration let X be real-functions-membered set; cluster (-)X -> real-functions-membered; coherence proof let x; assume A1: x in (-)X; then reconsider x as Element of (-)X; A2: -x in X by A1,Th24; --x = x & (-)(-)X = X; hence thesis by A2; end; end; theorem Th25: for X being Subset of TOP-REAL n holds -X = (-)X proof set T = TOP-REAL n; let X be Subset of T; for f being complex-valued Function holds -f in -X iff f in X proof let f be complex-valued Function; hereby assume -f in -X; then consider v being Element of T such that A1: -f = (-1)*v and A2: v in X; reconsider g = -f as Element of T by A1; -g = --v by A1,RLVECT_1:29 .= v; hence f in X by A2; end; assume A3: f in X; then reconsider g = f as Element of T; -g = (-1)*g by RLVECT_1:29; hence thesis by A3; end; hence thesis by Def3; end; definition let n; let X be Subset of TOP-REAL n; redefine func (-)X -> Subset of TOP-REAL n; coherence proof -X = (-)X by Th25; hence thesis; end; end; registration let n; let X be open Subset of TOP-REAL n; cluster (-)X -> open Subset of TOP-REAL n; coherence proof reconsider n as Element of NAT by ORDINAL1:def 13; reconsider Y = (-)X as Subset of TOP-REAL n; for p being Point of TOP-REAL n st p in Y ex r being positive (real number) st Ball(p,r) c= Y proof let p be Point of TOP-REAL n; assume p in Y; then -(p qua real-valued Function) in (-)Y by Def3; then consider r being positive (real number) such that A1: Ball(-p,r) c= X by TOPS_4:2; take r; let x be Element of TOP-REAL n; assume x in Ball(p,r); then -x in Ball(-p,r) by Th23; hence thesis by A1,Th24; end; hence thesis by TOPS_4:2; end; end; definition let n, p, x; redefine func p.x -> Element of REAL; coherence by XREAL_0:def 1; end; definition let R,S,T be non empty TopSpace, f be Function of [:R,S:],T; let x be Point of [:R,S:]; redefine func f.x -> Point of T; coherence proof consider x1 being Point of R, x2 being Point of S such that A1: x = [x1,x2] by BORSUK_1:50; f. [x1,x2] is Point of T; hence thesis by A1; end; end; definition let R,S,T be non empty TopSpace, f be Function of [:R,S:],T; let r be Point of R, s be Point of S; redefine func f.(r,s) -> Point of T; coherence proof f.(r,s) = f. [r,s]; hence thesis; end; end; definition let n, p, r; redefine func p + r -> Point of TOP-REAL n; coherence proof A1: p+r is FinSequence of REAL by Th19; A2: len p = n by FINSEQ_1:def 18; Seg len (p+r) = dom (p+r) by FINSEQ_1:def 3 .= dom p by VALUED_1:def 2 .= Seg n by A2,FINSEQ_1:def 3; then len (p+r) = n by FINSEQ_1:8; then p+r is Element of REAL n by A1,FINSEQ_2:110; hence thesis by EUCLID:25; end; end; definition let n, p, r; redefine func p - r -> Point of TOP-REAL n; coherence proof p+-r is Point of TOP-REAL n; hence thesis; end; end; definition let n, p, r; redefine func p (#) r -> Point of TOP-REAL n; coherence proof A1: p(#)r is FinSequence of REAL by Th19; A2: len p = n by FINSEQ_1:def 18; Seg len (p(#)r) = dom (p(#)r) by FINSEQ_1:def 3 .= dom p by VALUED_1:def 5 .= Seg n by A2,FINSEQ_1:def 3; then len (p(#)r) = n by FINSEQ_1:8; then p(#)r is Element of REAL n by A1,FINSEQ_2:110; hence thesis by EUCLID:25; end; end; definition let n, p, r; redefine func p (/) r -> Point of TOP-REAL n; coherence proof reconsider f = p as Element of REAL n by EUCLID:25; f(/)r is Element of REAL n; hence thesis by EUCLID:25; end; end; definition let n; let p1, p2 be Point of TOP-REAL n; redefine func p1 (#) p2 -> Point of TOP-REAL n; coherence proof A1: p1(#)p2 is FinSequence of REAL by Th19; A2: len p1 = n & len p2 = n by FINSEQ_1:def 18; Seg len (p1(#)p2) = dom (p1(#)p2) by FINSEQ_1:def 3 .= dom p1 /\ dom p2 by VALUED_1:def 4 .= Seg n /\ dom p2 by A2,FINSEQ_1:def 3 .= Seg n /\ Seg n by A2,FINSEQ_1:def 3; then len (p1(#)p2) = n by FINSEQ_1:8; then p1(#)p2 is Element of REAL n by A1,FINSEQ_2:110; hence thesis by EUCLID:25; end; commutativity; end; definition let n; let p be Point of TOP-REAL n; redefine func sqr p -> Point of TOP-REAL n; coherence proof sqr p = p(#)p; hence thesis; end; end; definition let n; let p1, p2 be Point of TOP-REAL n; redefine func p1 /" p2 -> Point of TOP-REAL n; coherence proof A1: p1/"p2 is FinSequence of REAL by Th19; A2: len p1 = n & len p2 = n by FINSEQ_1:def 18; Seg len (p1/"p2) = dom (p1/"p2) by FINSEQ_1:def 3 .= dom p1 /\ dom p2 by VALUED_1:16 .= Seg n /\ dom p2 by A2,FINSEQ_1:def 3 .= Seg n /\ Seg n by A2,FINSEQ_1:def 3; then len (p1/"p2) = n by FINSEQ_1:8; then p1/"p2 is Element of REAL n by A1,FINSEQ_2:110; hence thesis by EUCLID:25; end; end; definition let n, p, x, r; redefine func p+*(x,r) -> Point of TOP-REAL n; coherence proof A1: p+*(x,r) is FinSequence of REAL by Th19; A2: len p = n by FINSEQ_1:def 18; Seg len (p+*(x,r)) = dom (p+*(x,r)) by FINSEQ_1:def 3 .= dom p by FUNCT_7:32 .= Seg n by A2,FINSEQ_1:def 3; then len (p+*(x,r)) = n by FINSEQ_1:8; then p+*(x,r) is Element of REAL n by A1,FINSEQ_2:110; hence thesis by EUCLID:25; end; end; theorem for a, o being Point of TOP-REAL n holds n <> 0 & a in Ball(o,r) implies abs Sum(a-o) < n*r proof let a, o be Point of TOP-REAL n; set R1 = a-o, R2 = n|->r; assume that A1: n <> 0 and A2: a in Ball(o,r); A3: Sum R2 = n*r by RVSUM_1:110; A4: abs R1 is Element of n-tuples_on REAL & R2 is Element of n-tuples_on REAL by Lm1; A5: for j being Nat st j in Seg n holds (abs R1).j < R2.j proof let j be Nat; assume j in Seg n; then A6: R2.j = r by FINSEQ_2:71; abs(R1.j) < r by A2,EUCLID_9:9; hence thesis by A6,VALUED_1:18; end; then A7: for j being Nat st j in Seg n holds (abs R1).j <= R2.j; ex j being Nat st j in Seg n & (abs R1).j < R2.j proof take 1; 1 <= n by A1,NAT_1:14; hence 1 in Seg n; hence thesis by A5; end; then A8: Sum abs R1 < Sum R2 by A7,A4,RVSUM_1:113; abs Sum R1 <= Sum abs R1 by Th21; hence thesis by A3,A8,XXREAL_0:2; end; registration let n; cluster Euclid n -> real-functions-membered; coherence proof let x; assume x in the carrier of Euclid n; then reconsider x as Point of Euclid n; x is real-valued; hence thesis; end; end; theorem for V being add-associative right_zeroed right_complementable (non empty addLoopStr), v,u being Element of V holds v + u - u = v proof let V be add-associative right_zeroed right_complementable (non empty addLoopStr), v,u be Element of V; thus v + u - u = v + (u-u) by RLVECT_1:42 .= v + 0.V by RLVECT_1:16 .= v by RLVECT_1:10; end; theorem for V being Abelian add-associative right_zeroed right_complementable (non empty addLoopStr), v,u being Element of V holds v - u + u = v proof let V be Abelian add-associative right_zeroed right_complementable (non empty addLoopStr), v,u be Element of V; thus v - u + u = v - (u-u) by RLVECT_1:43 .= v - 0.V by RLVECT_1:16 .= v by RLVECT_1:26; end; theorem Th29: for Y being complex-functions-membered set, f being PartFunc of X,Y holds f[+]c = f<+>(dom f-->c) proof let Y be complex-functions-membered set, f be PartFunc of X,Y; set g = dom f-->c; A1: dom (f[+]c) = dom f by VALUED_2:def 37; A2: dom (f<+>g) = dom f /\ dom g by VALUED_2:def 41; A3: dom g = dom f by FUNCOP_1:19; now let x; assume A4: x in dom (f[+]c); hence (f[+]c).x = f.x+c by VALUED_2:def 37 .= f.x+g.x by A1,A4,FUNCOP_1:13 .= (f<+>g).x by A1,A2,A3,A4,VALUED_2:def 41; end; hence thesis by A1,A2,A3,FUNCT_1:9; end; theorem for Y being complex-functions-membered set, f being PartFunc of X,Y holds f[-]c = f<->(dom f-->c) proof let Y be complex-functions-membered set, f be PartFunc of X,Y; set g = dom f-->c; A1: dom (f[-]c) = dom f by VALUED_2:def 37; A2: dom (f<->g) = dom f /\ dom g by VALUED_2:61; A3: dom g = dom f by FUNCOP_1:19; now let x; assume A4: x in dom (f[-]c); hence (f[-]c).x = f.x-c by VALUED_2:def 37 .= f.x-g.x by A1,A4,FUNCOP_1:13 .= (f<->g).x by A1,A2,A3,A4,VALUED_2:62; end; hence thesis by A1,A2,A3,FUNCT_1:9; end; theorem Th31: for Y being complex-functions-membered set, f being PartFunc of X,Y holds f[#]c = f<#>(dom f-->c) proof let Y be complex-functions-membered set, f be PartFunc of X,Y; set g = dom f-->c; A1: dom (f[#]c) = dom f by VALUED_2:def 39; A2: dom (f<#>g) = dom f /\ dom g by VALUED_2:def 43; A3: dom g = dom f by FUNCOP_1:19; now let x; assume A4: x in dom (f[#]c); hence (f[#]c).x = c(#)(f.x) by VALUED_2:def 39 .= (f.x)(#)(g.x) by A1,A4,FUNCOP_1:13 .= (f<#>g).x by A1,A2,A3,A4,VALUED_2:def 43; end; hence thesis by A1,A2,A3,FUNCT_1:9; end; theorem for Y being complex-functions-membered set, f being PartFunc of X,Y holds f[/]c = f(dom f-->c) proof let Y be complex-functions-membered set, f be PartFunc of X,Y; set g = dom f-->c; A1: dom (f[/]c) = dom f by VALUED_2:def 39; A2: dom (fg) = dom f /\ dom g by VALUED_2:71; A3: dom g = dom f by FUNCOP_1:19; now let x; assume A4: x in dom (f[/]c); hence (f[/]c).x = (f.x)(/)c by VALUED_2:56 .= (f.x)(/)(g.x) by A1,A4,FUNCOP_1:13 .= (fg).x by A1,A2,A3,A4,VALUED_2:72; end; hence thesis by A1,A2,A3,FUNCT_1:9; end; registration let D be complex-functions-membered set; let f, g be FinSequence of D; cluster f<++>g -> FinSequence-like; coherence proof dom(f<++>g) = dom f /\ dom g by VALUED_2:def 45; hence thesis by VALUED_1:19; end; cluster f<-->g -> FinSequence-like; coherence proof dom(f<-->g) = dom f /\ dom g by VALUED_2:def 46; hence thesis by VALUED_1:19; end; cluster f<##>g -> FinSequence-like; coherence proof dom(f<##>g) = dom f /\ dom g by VALUED_2:def 47; hence thesis by VALUED_1:19; end; cluster fg -> FinSequence-like; coherence proof dom(fg) = dom f /\ dom g by VALUED_2:def 48; hence thesis by VALUED_1:19; end; end; theorem for f being Function of X,TOP-REAL n holds <->f is Function of X,TOP-REAL n proof let f be Function of X,TOP-REAL n; set g = <->f; A1: dom g = dom f by VALUED_2:def 33; A2: dom f = X by FUNCT_2:def 1; for x st x in X holds g.x in the carrier of TOP-REAL n proof let x; assume A3: x in X; then reconsider X as non empty set; reconsider x as Element of X by A3; reconsider f as Function of X,TOP-REAL n; A4: -((f.x) qua real-valued Function) = -f.x; g.x = -((f.x) qua real-valued Function) by A1,A2,VALUED_2:def 33; hence thesis by A4; end; hence thesis by A1,A2,FUNCT_2:5; end; theorem Th34: for f being Function of TOP-REAL i,TOP-REAL n holds f(-) is Function of TOP-REAL i,TOP-REAL n proof set X = the carrier of TOP-REAL i; let f be Function of X,TOP-REAL n; set g = f(-); A1: dom g = dom f by VALUED_2:def 34; A2: dom f = X by FUNCT_2:def 1; for x st x in X holds g.x in the carrier of TOP-REAL n proof let x; assume x in X; then reconsider x as Element of X; reconsider y = -x as Element of X; reconsider f as Function of X,TOP-REAL n; g.x = f.y by A1,A2,VALUED_2:def 34; hence thesis; end; hence thesis by A1,A2,FUNCT_2:5; end; theorem Th35: for f being Function of X,TOP-REAL n holds f[+]r is Function of X,TOP-REAL n proof let f be Function of X,TOP-REAL n; set h = f[+]r; dom f = X by FUNCT_2:def 1; then A1: dom h = X by VALUED_2:def 37; for x st x in X holds h.x in the carrier of TOP-REAL n proof let x; assume A2: x in X; then reconsider X as non empty set; reconsider x as Element of X by A2; reconsider f as Function of X,TOP-REAL n; A3: ((f.x) qua real-valued Function)+r = f.x+r; h.x = ((f.x) qua real-valued Function)+r by A1,VALUED_2:def 37; hence thesis by A3; end; hence thesis by A1,FUNCT_2:5; end; theorem for f being Function of X,TOP-REAL n holds f[-]r is Function of X,TOP-REAL n by Th35; theorem Th37: for f being Function of X,TOP-REAL n holds f[#]r is Function of X,TOP-REAL n proof let f be Function of X,TOP-REAL n; set h = f[#]r; dom f = X by FUNCT_2:def 1; then A1: dom h = X by VALUED_2:def 39; for x st x in X holds h.x in the carrier of TOP-REAL n proof let x; assume A2: x in X; then reconsider X as non empty set; reconsider x as Element of X by A2; reconsider f as Function of X,TOP-REAL n; A3: ((f.x) qua real-valued Function)(#)r = f.x(#)r; h.x = ((f.x) qua real-valued Function)(#)r by A1,VALUED_2:def 39; hence thesis by A3; end; hence thesis by A1,FUNCT_2:5; end; theorem for f being Function of X,TOP-REAL n holds f[/]r is Function of X,TOP-REAL n by Th37; theorem Th39: for f, g being Function of X,TOP-REAL n holds f<++>g is Function of X,TOP-REAL n proof let f, g be Function of X,TOP-REAL n; set h = f<++>g; A1: dom f = X by FUNCT_2:def 1; dom g = X by FUNCT_2:def 1; then A2: dom h = X by A1,VALUED_2:def 45; for x st x in X holds h.x in the carrier of TOP-REAL n proof let x; assume A3: x in X; then reconsider X as non empty set; reconsider x as Element of X by A3; reconsider f, g as Function of X,TOP-REAL n; A4: ((f.x) qua real-valued Function)+g.x = f.x+g.x; h.x = ((f.x) qua real-valued Function)+g.x by A2,VALUED_2:def 45; hence thesis by A4; end; hence thesis by A2,FUNCT_2:5; end; theorem Th40: for f, g being Function of X,TOP-REAL n holds f<-->g is Function of X,TOP-REAL n proof let f, g be Function of X,TOP-REAL n; set h = f<-->g; A1: dom f = X by FUNCT_2:def 1; dom g = X by FUNCT_2:def 1; then A2: dom h = X by A1,VALUED_2:def 46; for x st x in X holds h.x in the carrier of TOP-REAL n proof let x; assume A3: x in X; then reconsider X as non empty set; reconsider x as Element of X by A3; reconsider f, g as Function of X,TOP-REAL n; A4: ((f.x) qua real-valued Function)-g.x = f.x-g.x; h.x = ((f.x) qua real-valued Function)-g.x by A2,VALUED_2:def 46; hence thesis by A4; end; hence thesis by A2,FUNCT_2:5; end; theorem Th41: for f, g being Function of X,TOP-REAL n holds f<##>g is Function of X,TOP-REAL n proof let f, g be Function of X,TOP-REAL n; set h = f<##>g; A1: dom f = X by FUNCT_2:def 1; dom g = X by FUNCT_2:def 1; then A2: dom h = X by A1,VALUED_2:def 47; for x st x in X holds h.x in the carrier of TOP-REAL n proof let x; assume A3: x in X; then reconsider X as non empty set; reconsider x as Element of X by A3; reconsider f, g as Function of X,TOP-REAL n; h.x = f.x(#)g.x by A2,VALUED_2:def 47; hence thesis; end; hence thesis by A2,FUNCT_2:5; end; theorem Th42: for f, g being Function of X,TOP-REAL n holds fg is Function of X,TOP-REAL n proof let f, g be Function of X,TOP-REAL n; set h = fg; A1: dom f = X by FUNCT_2:def 1; dom g = X by FUNCT_2:def 1; then A2: dom h = X by A1,VALUED_2:def 48; for x st x in X holds h.x in the carrier of TOP-REAL n proof let x; assume A3: x in X; then reconsider X as non empty set; reconsider x as Element of X by A3; reconsider f, g as Function of X,TOP-REAL n; h.x = f.x /" g.x by A2,VALUED_2:def 48; hence thesis; end; hence thesis by A2,FUNCT_2:5; end; theorem Th43: for f being Function of X,TOP-REAL n, g being Function of X,R^1 holds f<+>g is Function of X,TOP-REAL n proof let f be Function of X,TOP-REAL n, g be Function of X,R^1; set h = f<+>g; A1: dom f = X by FUNCT_2:def 1; dom g = X by FUNCT_2:def 1; then A2: dom h = X by A1,VALUED_2:def 41; for x st x in X holds h.x in the carrier of TOP-REAL n proof let x; assume A3: x in X; then reconsider X as non empty set; reconsider x as Element of X by A3; reconsider f as Function of X,TOP-REAL n; h.x = f.x+g.x by A2,VALUED_2:def 41; hence thesis; end; hence thesis by A2,FUNCT_2:5; end; theorem Th44: for f being Function of X,TOP-REAL n, g being Function of X,R^1 holds f<->g is Function of X,TOP-REAL n proof let f be Function of X,TOP-REAL n, g be Function of X,R^1; set h = f<->g; A1: dom f = X by FUNCT_2:def 1; dom g = X by FUNCT_2:def 1; then A2: dom h = X by A1,VALUED_2:61; for x st x in X holds h.x in the carrier of TOP-REAL n proof let x; assume A3: x in X; then reconsider X as non empty set; reconsider x as Element of X by A3; reconsider f as Function of X,TOP-REAL n; h.x = f.x-g.x by A2,VALUED_2:62; hence thesis; end; hence thesis by A2,FUNCT_2:5; end; theorem Th45: for f being Function of X,TOP-REAL n, g being Function of X,R^1 holds f<#>g is Function of X,TOP-REAL n proof let f be Function of X,TOP-REAL n, g be Function of X,R^1; set h = f<#>g; A1: dom f = X by FUNCT_2:def 1; dom g = X by FUNCT_2:def 1; then A2: dom h = X by A1,VALUED_2:def 43; for x st x in X holds h.x in the carrier of TOP-REAL n proof let x; assume A3: x in X; then reconsider X as non empty set; reconsider x as Element of X by A3; reconsider f as Function of X,TOP-REAL n; h.x = f.x(#)g.x by A2,VALUED_2:def 43; hence thesis; end; hence thesis by A2,FUNCT_2:5; end; theorem Th46: for f being Function of X,TOP-REAL n, g being Function of X,R^1 holds fg is Function of X,TOP-REAL n proof let f be Function of X,TOP-REAL n, g be Function of X,R^1; set h = fg; A1: dom f = X by FUNCT_2:def 1; dom g = X by FUNCT_2:def 1; then A2: dom h = X by A1,VALUED_2:71; for x st x in X holds h.x in the carrier of TOP-REAL n proof let x; assume A3: x in X; then reconsider X as non empty set; reconsider x as Element of X by A3; reconsider f as Function of X,TOP-REAL n; h.x = f.x(/)g.x by A2,VALUED_2:72; hence thesis; end; hence thesis by A2,FUNCT_2:5; end; definition let n be Nat; let T be non empty set; let R be real-membered set; let f be Function of T,R; func incl(f,n) -> Function of T,TOP-REAL n means :Def4: for t being Element of T holds it.t = n |-> f.t; existence proof defpred P[set,set] means $2 = n |-> f.$1; A1: for x being Element of T ex y being Element of TOP-REAL n st P[x,y] proof let x be Element of T; f.x in REAL by XREAL_0:def 1; then n |-> f.x is Element of REAL n by FINSEQ_2:132; then reconsider y = n |-> f.x as Point of TOP-REAL n by EUCLID:25; take y; thus thesis; end; ex F being Function of T,TOP-REAL n st for x being Element of T holds P[x,F.x] from FUNCT_2:sch 3(A1); hence thesis; end; uniqueness proof let F, G be Function of T,TOP-REAL n such that A2: for t being Element of T holds F.t = n |-> f.t and A3: for t being Element of T holds G.t = n |-> f.t; let t be Element of T; thus F.t = n |-> f.t by A2 .= G.t by A3; end; end; theorem Th47: for R being real-membered set for f being Function of T,R, t being Point of T st x in Seg n holds incl(f,n).t.x = f.t proof let R be real-membered set; let f be Function of T,R; let t be Point of T; assume A1: x in Seg n; thus incl(f,n).t.x = (n |-> f.t).x by Def4 .= f.t by A1,FINSEQ_2:71; end; theorem Th48: for T being non empty set, R being real-membered set, f being Function of T,R holds incl(f,0) = T --> 0 proof let T be non empty set; let R be real-membered set; let f be Function of T,R; reconsider z = 0 as Element of TOP-REAL 0; incl(f,0) = T --> z proof let x be Element of T; thus incl(f,0).x = (T --> z).x; end; hence thesis; end; theorem Th49: for f being Function of T,TOP-REAL n, g being Function of T,R^1 holds f<+>g = f<++>incl(g,n) proof let f be Function of T,TOP-REAL n; let g be Function of T,R^1; set I = incl(g,n); reconsider h = f<+>g as Function of T,TOP-REAL n by Th43; reconsider G = f<++>I as Function of T,TOP-REAL n by Th39; h = G proof let t be Point of T; A1: dom h = the carrier of T by FUNCT_2:def 1; A2: f.t + I.t = f.t + g.t proof A3: dom (f.t) = Seg n & dom (I.t) = Seg n by EUCLID:3; A4: dom (f.t + I.t) = dom (f.t) /\ dom (I.t) by VALUED_1:def 1 .= Seg n by A3; A5: dom (f.t + g.t) = dom (f.t) by VALUED_1:def 2; thus dom (f.t + I.t) = dom (f.t + g.t) by A4,EUCLID:3; let x; assume A6: x in dom (f.t + I.t); hence (f.t + I.t).x = f.t.x + I.t.x by VALUED_1:def 1 .= f.t.x + g.t by A4,A6,Th47 .= (f.t + g.t).x by A3,A4,A6,A5,VALUED_1:def 2; end; dom G = the carrier of T by FUNCT_2:def 1; hence G.t = f.t + I.t by VALUED_2:def 45 .= h.t by A1,A2,VALUED_2:def 41; end; hence thesis; end; theorem Th50: for f being Function of T,TOP-REAL n, g being Function of T,R^1 holds f<->g = f<-->incl(g,n) proof let f be Function of T,TOP-REAL n; let g be Function of T,R^1; set I = incl(g,n); reconsider h = f<->g as Function of T,TOP-REAL n by Th44; reconsider G = f<-->I as Function of T,TOP-REAL n by Th40; h = G proof let t be Point of T; A1: dom h = the carrier of T by FUNCT_2:def 1; A2: f.t - I.t = f.t - g.t proof A3: dom (f.t) = Seg n & dom (I.t) = Seg n by EUCLID:3; A4: dom (f.t - I.t) = dom (f.t) /\ dom (I.t) by VALUED_1:12 .= Seg n by A3; A5: dom (f.t - g.t) = dom (f.t) by VALUED_1:def 2; thus dom (f.t - I.t) = dom (f.t - g.t) by A4,EUCLID:3; let x; assume A6: x in dom (f.t - I.t); hence (f.t - I.t).x = f.t.x - I.t.x by VALUED_1:13 .= f.t.x - g.t by A4,A6,Th47 .= (f.t - g.t).x by A3,A4,A6,A5,VALUED_1:def 2; end; dom G = the carrier of T by FUNCT_2:def 1; hence G.t = f.t - I.t by VALUED_2:def 46 .= h.t by A1,A2,VALUED_2:62; end; hence thesis; end; theorem Th51: for f being Function of T,TOP-REAL n, g being Function of T,R^1 holds f<#>g = f<##>incl(g,n) proof let f be Function of T,TOP-REAL n; let g be Function of T,R^1; set I = incl(g,n); reconsider h = f<#>g as Function of T,TOP-REAL n by Th45; reconsider G = f<##>I as Function of T,TOP-REAL n by Th41; h = G proof let t be Point of T; A1: dom h = the carrier of T by FUNCT_2:def 1; A2: f.t (#) I.t = f.t (#) g.t proof A3: dom (f.t) = Seg n & dom (I.t) = Seg n by EUCLID:3; A4: dom (f.t (#) I.t) = dom (f.t) /\ dom (I.t) by VALUED_1:def 4 .= Seg n by A3; hence dom (f.t (#) I.t) = dom (f.t (#) g.t) by EUCLID:3; let x; assume A5: x in dom (f.t (#) I.t); hence (f.t (#) I.t).x = f.t.x * I.t.x by VALUED_1:def 4 .= f.t.x * g.t by A4,A5,Th47 .= (f.t (#) g.t).x by VALUED_1:6; end; dom G = the carrier of T by FUNCT_2:def 1; hence G.t = f.t (#) I.t by VALUED_2:def 47 .= h.t by A1,A2,VALUED_2:def 43; end; hence thesis; end; theorem for f being Function of T,TOP-REAL n, g being Function of T,R^1 holds fg = fincl(g,n) proof let f be Function of T,TOP-REAL n; let g be Function of T,R^1; set I = incl(g,n); reconsider h = fg as Function of T,TOP-REAL n by Th46; reconsider G = fI as Function of T,TOP-REAL n by Th42; h = G proof let t be Point of T; A1: dom h = the carrier of T by FUNCT_2:def 1; A2: f.t /" I.t = f.t (#) (g".t) proof A3: dom (f.t) = Seg n & dom (I.t) = Seg n by EUCLID:3; A4: dom (f.t /" I.t) = dom (f.t) /\ dom (I.t) by VALUED_1:16 .= Seg n by A3; hence dom (f.t /" I.t) = dom (f.t (#) g".t) by EUCLID:3; let x; assume A5: x in dom (f.t /" I.t); thus (f.t /" I.t).x = f.t.x / I.t.x by VALUED_1:17 .= f.t.x / g.t by A4,A5,Th47 .= f.t.x * (g".t) by VALUED_1:10 .= (f.t (#) g".t).x by VALUED_1:6; end; dom G = the carrier of T by FUNCT_2:def 1; hence G.t = f.t /" I.t by VALUED_2:def 48 .= h.t by A1,A2,VALUED_2:def 43; end; hence thesis; end; definition let n; set T = TOP-REAL n; set c = the carrier of T; A1: the carrier of [:T,T:] = [:c,c:] by BORSUK_1:def 5; func TIMES(n) -> Function of [:TOP-REAL n,TOP-REAL n:],TOP-REAL n means :Def5: for x,y being Point of TOP-REAL n holds it.(x,y) = x(#)y; existence proof deffunc F(Point of T,Point of T) = $1(#)$2; ex f being Function of [:c,c:],c st for x,y being Element of c holds f.(x,y) = F(x,y) from BINOP_1:sch 4; hence thesis by A1; end; uniqueness proof let f,g be Function of [:T,T:],T such that A2: for x,y being Point of T holds f.(x,y) = x(#)y and A3: for x,y being Point of T holds g.(x,y) = x(#)y; now let x,y be Point of T; thus f.(x,y) = x(#)y by A2 .= g.(x,y) by A3; end; hence thesis by A1,BINOP_1:2; end; end; theorem Th53: TIMES(0) = [:TOP-REAL 0,TOP-REAL 0:] --> 0.TOP-REAL 0 proof set T = TOP-REAL 0; let x be Element of the carrier of [:T,T:]; thus TIMES(0).x = ([:T,T:] --> 0.T).x; end; theorem Th54: for f, g being Function of T,TOP-REAL n holds f <##> g = TIMES(n).:(f,g) proof set R = TOP-REAL n; set F = TIMES(n); let f, g be Function of T,R; A1: dom(f<##>g) = dom f /\ dom g by VALUED_2:def 47; dom F = the carrier of [:R,R:] by FUNCT_2:def 1 .= [:the carrier of R,the carrier of R:] by BORSUK_1:def 5; then [:rng f, rng g:] c= dom F by ZFMISC_1:119; then A2: dom(F.:(f,g)) = dom f /\ dom g by FUNCOP_1:84; now let x; assume A3: x in dom (f<##>g); then A4: f.x is Point of R & g.x is Point of R by FUNCT_2:7; thus (f<##>g).x = f.x(#)g.x by A3,VALUED_2:def 47 .= F.(f.x,g.x) by A4,Def5 .= F.:(f,g).x by A1,A2,A3,FUNCOP_1:28; end; hence thesis by A1,A2,FUNCT_1:9; end; definition let m, n; A1: m in NAT & n in NAT by ORDINAL1:def 13; func PROJ(m,n) -> Function of TOP-REAL m,R^1 means :Def6: for p being Element of TOP-REAL m holds it.p = p/.n; existence by A1,JORDAN2B:1; uniqueness proof let F, G be Function of TOP-REAL m,R^1 such that A2: for p being Element of TOP-REAL m holds F.p = p/.n and A3: for p being Element of TOP-REAL m holds G.p = p/.n; let p be Element of TOP-REAL m; thus F.p = p/.n by A2 .= G.p by A3; end; end; theorem Th55: for p being Point of TOP-REAL m st n in dom p holds PROJ(m,n).:Ball(p,r) = ]. p/.n-r , p/.n+r .[ proof let p be Point of TOP-REAL m such that A1: n in dom p; A2: m in NAT by ORDINAL1:def 13; per cases; suppose A3: r <= 0; then ]. p/.n-r , p/.n+r .[ = {}; hence thesis by A3; end; suppose A4: 0 < r; A5: dom p = Seg m by EUCLID:3; thus PROJ(m,n).:Ball(p,r) c= ]. p/.n-r , p/.n+r .[ proof let y be set; assume y in PROJ(m,n).:Ball(p,r); then consider x being Element of TOP-REAL m such that A6: x in Ball(p,r) and A7: y = PROJ(m,n).x by FUNCT_2:116; A8: PROJ(m,n).x = x/.n by Def6; A9: |.x-p.| < r by A2,A6,TOPREAL9:7; 0 <= Sum sqr (x-p) by RVSUM_1:116; then (sqrt Sum sqr (x-p))^2 = Sum sqr (x-p) by SQUARE_1:def 4; then A10: Sum sqr (x-p) < r^2 by A9,SQUARE_1:78; dom x = Seg m by EUCLID:3; then (x/.n - p/.n)^2 <= Sum sqr (x-p) by A5,A1,EUCLID_9:8; then (x/.n - p/.n)^2 < r^2 by A10,XXREAL_0:2; then -r < x/.n - p/.n & x/.n - p/.n < r by A4,SQUARE_1:118; then -r + p/.n < x/.n - p/.n + p/.n & x/.n - p/.n + p/.n < r + p/.n by XREAL_1:8; hence thesis by A7,A8,XXREAL_1:4; end; let y be set; assume A11: y in ]. p/.n-r , p/.n+r .[; then reconsider y as Element of REAL; set x = p+*(n,y); reconsider X = x as FinSequence of REAL by EUCLID:27; A12: dom X = dom p by FUNCT_7:32; A13: p/.n = p.n by A1,PARTFUN1:def 8; p/.n-r < y & y < p/.n+r by A11,XXREAL_1:4; then A14: y - p/.n < r & -r < y - p/.n by XREAL_1:21,22; x-p = (0*m)+*(n,y-p.n) by Th17; then |.x-p.| = abs(y-p.n) by A1,A5,Th13; then |.x-p.| < r by A13,A14,SEQ_2:9; then A15: x in Ball(p,r) by A2,TOPREAL9:7; PROJ(m,n).x = x/.n by Def6 .= X.n by A12,A1,PARTFUN1:def 8 .= y by A1,FUNCT_7:33; hence thesis by A15,FUNCT_2:43; end; end; theorem for m being non zero Nat for f being Function of T,R^1 holds f = PROJ(m,m) * incl(f,m) proof let m be non zero Nat; let f be Function of T,R^1; let p be Point of T; set I = incl(f,m); reconsider G = m|->f.p as FinSequence of REAL; A1: m in NAT by ORDINAL1:def 13; 1 <= m by NAT_1:14; then A2: m in Seg m by A1; A3: dom (m|->f.p) = Seg m by FUNCOP_1:19; thus (PROJ(m,m)*I).p = PROJ(m,m).(I.p) by FUNCT_2:21 .= I.p/.m by Def6 .= G/.m by Def4 .= G.m by A2,A3,PARTFUN1:def 8 .= f.p by A2,FINSEQ_2:71; end; begin :: Continuity registration let T; cluster non-empty continuous Function of T,R^1; existence proof take T --> R^1(1); thus thesis; end; end; theorem n in Seg m implies PROJ(m,n) is continuous proof assume A1: n in Seg m; A2: m in NAT by ORDINAL1:def 13; for p being Element of TOP-REAL m holds PROJ(m,n).p = p/.n by Def6; hence thesis by A2,A1,JORDAN2B:22; end; theorem n in Seg m implies PROJ(m,n) is open proof set f = PROJ(m,n); assume A1: n in Seg m; for p being Point of TOP-REAL m, r being positive (real number) holds ex s being positive (real number) st ].f.p-s,f.p+s.[ c= f.:Ball(p,r) proof let p be Point of TOP-REAL m, r be positive (real number); take r; A2: dom p = Seg m by EUCLID:3; p/.n = f.p by Def6; hence thesis by A2,A1,Th55; end; hence thesis by TOPS_4:13; end; registration let n,T; let f be continuous Function of T,R^1; cluster incl(f,n) -> continuous; coherence proof reconsider n as Element of NAT by ORDINAL1:def 13; set g = incl(f,n); per cases; suppose A1: n = 0; then reconsider z = 0 as Element of TOP-REAL n; incl(f,0) = T --> z by Th48; hence thesis by A1; end; suppose A2: n > 0; for p being Point of T, V being Subset of TOP-REAL n st g.p in V & V is open holds ex W being Subset of T st p in W & W is open & g.:W c= V proof let p be Point of T, V be Subset of TOP-REAL n; assume that A3: g.p in V and A4: V is open; A5: g.p in Int V by A3,A4,TOPS_1:55; reconsider s = g.p as Point of Euclid n by EUCLID:71; consider r being real number such that A6: r > 0 and A7: Ball(s,r) c= V by A5,GOBOARD6:8; reconsider G = n|->f.p as FinSequence of REAL; 1 <= n by A2,NAT_1:14; then A8: n in Seg n; reconsider F = g.p as FinSequence of REAL by EUCLID:27; A9: F = n|->f.p by Def4; A10: dom (n|->f.p) = Seg n by FUNCOP_1:19; A11: g.p/.n = G/.n by Def4 .= G.n by A8,A10,PARTFUN1:def 8 .= f.p by A8,FINSEQ_2:71; set R = r/sqrt n; set RR = R^1(].g.p/.n-r/sqrt n,g.p/.n+r/sqrt n.[); f.p in RR by A2,A11,A6,TOPREAL6:20; then consider W being Subset of T such that A12: p in W & W is open and A13: f.:W c= RR by JGRAPH_2:20; take W; thus p in W & W is open by A12; let y be Element of TOP-REAL n; assume y in g.:W; then consider x being Element of T such that A14: x in W and A15: g.x = y by FUNCT_2:116; reconsider y1 = y as Point of Euclid n by EUCLID:71; reconsider y2 = y1, s2 = s as Element of REAL n; A16: y2 = n|->f.x by A15,Def4; A17: (Pitag_dist n).(y1,s) = |.y2-s2.| by EUCLID:def 6 .= (sqrt n) * abs(f.x-f.p) by A16,A9,Th11; f.x in f.:W by A14,FUNCT_2:43; then abs(f.x-f.p) < R by A13,A11,RCOMP_1:8; then dist(y1,s) < r by A2,A17,XREAL_1:81; then y in Ball(s,r) by METRIC_1:12; hence thesis by A7; end; hence thesis by JGRAPH_2:20; end; end; end; registration let n; cluster TIMES(n) -> continuous; coherence proof per cases; suppose n is non zero; then reconsider 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 T; A1: TopSpaceMetr Euclid n = product(J) by EUCLID_9:28; A2: the TopStruct of T = TopSpaceMetr Euclid n by EUCLID:def 8; then reconsider F as Function of [:T,T:], product J by EUCLID_9:28; A3: the carrier of T = REAL n by EUCLID:25; now let i be Element of Seg n; set P = proj(J,i); A4: J.i = R^1 by FUNCOP_1:13; reconsider f = P*F as Function of [:T,T:],R^1 by FUNCOP_1:13; A5: the carrier of [:T,T:] = [:c,c:] by BORSUK_1:def 5; A6: for a,b being Point of T holds f.(a,b) = a.i*b.i proof let a,b be Point of T; thus f.(a,b) = P.(F.(a,b)) by A5,BINOP_1:30 .= P.(a(#)b) by Def5 .= (a(#)b).i by A1,A2,YELLOW17:8 .= a.i*b.i by VALUED_1:5; end; deffunc F1(Element of c,Element of c) = $1.i; consider f1 being Function of [:c,c:],REAL such that A7: for a,b being Element of c holds f1.(a,b) = F1(a,b) from BINOP_1:sch 4; reconsider f1 as Function of [:T,T:],R^1 by A5; deffunc F2(Element of c,Element of c) = $2.i; consider f2 being Function of [:c,c:],REAL such that A8: for a,b being Element of c holds f2.(a,b) = F2(a,b) from BINOP_1:sch 4; reconsider f1,f2 as Function of [:T,T:],R^1 by A5; for p being Point of [:T,T:], r being positive (real number) ex W being open Subset of [:T,T:] st p in W & f1.:W c= ].f1.p-r,f1.p+r.[ proof let p be Point of [:T,T:], r be positive (real number); consider p1,p2 being Point of T such that A9: p = [p1,p2] by BORSUK_1:50; set B1 = Ball(p1,r), B2 = [#]T; reconsider W = [:B1,B2:] as open Subset of [:T,T:] by BORSUK_1:46; take W; p1 in B1 & p2 in B2 by TOPGEN_5:17; hence p in W by A9,ZFMISC_1:def 2; let y be set; assume y in f1.:W; then consider x being Point of [:T,T:] such that A10: x in W and A11: f1.x = y by FUNCT_2:116; consider x1,x2 being Point of T 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 B1 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; end; then A15: f1 is continuous by TOPS_4:21; for p being Point of [:T,T:], r being positive (real number) ex W being open Subset of [:T,T:] st p in W & f2.:W c= ].f2.p-r,f2.p+r.[ proof let p be Point of [:T,T:], r be positive (real number); consider p1,p2 being Point of T such that A16: p = [p1,p2] by BORSUK_1:50; set B1 = [#]T, B2 = Ball(p2,r); reconsider W = [:B1,B2:] as open Subset of [:T,T:] by BORSUK_1:46; take W; p1 in B1 & p2 in B2 by TOPGEN_5:17; hence p in W by A16,ZFMISC_1:def 2; let y be set; assume y in f2.:W; then consider x being Point of [:T,T:] such that A17: x in W and A18: f2.x = y by FUNCT_2:116; consider x1,x2 being Point of T such that A19: x = [x1,x2] by BORSUK_1:50; A20: f2.(x1,x2) = x2.i & f2.(p1,p2) = p2.i by A8; x2 in B2 by A17,A19,ZFMISC_1:106; then A21: |.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 A16,A19,A20,A21,XXREAL_0:2; hence y in ].f2.p-r,f2.p+r.[ by A18,RCOMP_1:8; end; then f2 is continuous by TOPS_4:21; then consider g being Function of [:T,T:],R^1 such that A22: for p being Point of [:T,T:], r1,r2 being real number st f1.p = r1 & f2.p = r2 holds g.p = r1*r2 and A23: g is continuous by A15,JGRAPH_2:35; now let a, b be Point of T; A24: 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 A22,A24 .= g.(a,b); end; hence P*F is continuous by A23,A4,A5,BINOP_1:2; end; then F is continuous by WAYBEL18:7; hence thesis by A1,A2,YELLOW12:36; end; suppose n is zero; hence thesis by Th53; end; end; end; theorem for f being Function of TOP-REAL m,TOP-REAL n st f is continuous holds f(-) is continuous Function of TOP-REAL m,TOP-REAL n proof let f be Function of TOP-REAL m,TOP-REAL n; assume A1: f is continuous; reconsider g = f(-) as Function of TOP-REAL m,TOP-REAL n by Th34; for p being Point of TOP-REAL m, r being positive (real number) ex s being positive (real number) st g.:Ball(p,s) c= Ball(g.p,r) proof let p be Point of TOP-REAL m; let r be positive (real number); consider s being positive (real number) such that A2: f.:Ball(-p,s) c= Ball(f.-p,r) by A1,TOPS_4:20; take s; let y be Element of TOP-REAL n; assume y in g.:Ball(p,s); then consider x being Element of TOP-REAL m such that A3: x in Ball(p,s) and A4: g.x = y by FUNCT_2:116; dom g = the carrier of TOP-REAL m by FUNCT_2:def 1; then A5: g.x = f.-x & g.p = f.-p by VALUED_2:def 34; -x in Ball(-p,s) by A3,Th23; then f.-x in f.:Ball(-p,s) by FUNCT_2:43; hence y in Ball(g.p,r) by A2,A4,A5; end; hence thesis by TOPS_4:20; end; registration let T; let f be continuous Function of T,R^1; cluster -f -> continuous Function of T,R^1; coherence proof let F be Function of T,R^1 such that A1: F = -f; consider g being Function of T,R^1 such that A2: for p being Point of T, r being real number st f.p = r holds g.p = -r and A3: g is continuous by JGRAPH_4:13; F = g proof let x be Point of T; thus F.x = -(f.x) by A1,VALUED_1:8 .= g.x by A2; end; hence thesis by A3; end; end; registration let T; let f be non-empty continuous Function of T,R^1; cluster f" -> continuous Function of T,R^1; coherence proof let F be Function of T,R^1 such that A1: F = f"; dom f = the carrier of T by FUNCT_2:def 1; then for q being Point of T holds f.q <> 0; then consider g being Function of T,R^1 such that A2: for p being Point of T, r being real number st f.p = r holds g.p = 1/r and A3: g is continuous by JGRAPH_2:36; F = g proof let x be Point of T; thus F.x = 1/(f.x) by A1,VALUED_1:10 .= g.x by A2; end; hence thesis by A3; end; end; registration let T; let f be continuous Function of T,R^1; let r; cluster f+r -> continuous Function of T,R^1; coherence proof let F be Function of T,R^1 such that A1: F = f+r; consider g being Function of T,R^1 such that A2: for p being Point of T, s being real number st f.p = s holds g.p = s + r and A3: g is continuous by JGRAPH_2:34; F = g proof let x be Point of T; thus F.x = (f.x)+r by A1,VALUED_1:2 .= g.x by A2; end; hence thesis by A3; end; cluster f-r -> continuous Function of T,R^1; coherence; cluster f(#)r -> continuous Function of T,R^1; coherence proof let F be Function of T,R^1 such that A4: F = f(#)r; consider g being Function of T,R^1 such that A5: for p being Point of T, s being real number st f.p = s holds g.p = r*s and A6: g is continuous by JGRAPH_2:33; F = g proof let x be Point of T; thus F.x = (f.x)*r by A4,VALUED_1:6 .= g.x by A5; end; hence thesis by A6; end; cluster f(/)r -> continuous Function of T,R^1; coherence; end; registration let T; let f, g be continuous Function of T,R^1; cluster f+g -> continuous Function of T,R^1; coherence proof let F be Function of T,R^1 such that A1: F = f+g; consider h being Function of T,R^1 such that A2: for p being Point of T, r1,r2 being real number st f.p = r1 & g.p = r2 holds h.p = r1 + r2 and A3: h is continuous by JGRAPH_2:29; F = h proof let x be Point of T; thus F.x = (f.x)+(g.x) by A1,VALUED_1:1 .= h.x by A2; end; hence thesis by A3; end; cluster f-g -> continuous Function of T,R^1; coherence proof f-g = f+-g; hence thesis; end; cluster f(#)g -> continuous Function of T,R^1; coherence proof let F be Function of T,R^1 such that A4: F = f(#)g; consider h being Function of T,R^1 such that A5: for p being Point of T, r1,r2 being real number st f.p = r1 & g.p = r2 holds h.p = r1 * r2 and A6: h is continuous by JGRAPH_2:35; F = h proof let x be Point of T; thus F.x = (f.x)*(g.x) by A4,VALUED_1:5 .= h.x by A5; end; hence thesis by A6; end; end; registration let T; let f be continuous Function of T,R^1; let g be non-empty continuous Function of T,R^1; cluster f /" g -> continuous Function of T,R^1; coherence proof f /" g = f(#)(g"); hence thesis; end; end; registration let n,T; let f, g be continuous Function of T,TOP-REAL n; cluster f<++>g -> continuous Function of T,TOP-REAL n; coherence proof let h be Function of T,TOP-REAL n such that A1: h = f<++>g; n in NAT by ORDINAL1:def 13; then consider F being Function of T,TOP-REAL n such that A2: for r being Point of T holds F.r = f.r + g.r and A3: F is continuous by JGRAPH_6:20; F = h proof A4: dom h = the carrier of T by FUNCT_2:def 1; let x be Point of T; thus F.x = f.x + g.x by A2 .= h.x by A1,A4,VALUED_2:def 45; end; hence thesis by A3; end; cluster f<-->g -> continuous Function of T,TOP-REAL n; coherence proof let h be Function of T,TOP-REAL n such that A5: h = f<-->g; A6: n in NAT by ORDINAL1:def 13; A7: for r being Point of T holds h.r = f.r - g.r proof let r be Point of T; dom h = the carrier of T by FUNCT_2:def 1; hence thesis by A5,VALUED_2:def 46; end; for p being Point of T, V being Subset of TOP-REAL n st h.p in V & V is open ex W being Subset of T st p in W & W is open & h.:W c= V proof let p be Point of T, V be Subset of TOP-REAL n; assume h.p in V & V is open; then A8: h.p in Int V by TOPS_1:55; reconsider r=h.p as Point of Euclid n by EUCLID:71; consider r0 being real number such that A9: r0>0 & Ball(r,r0) c= V by A6,A8,GOBOARD6:8; reconsider r01 = f.p as Point of Euclid n by EUCLID:71; reconsider G1 = Ball(r01,r0/2) as Subset of TOP-REAL n by EUCLID:71; A10: f.p in G1 by A9,GOBOARD6:4; A11: the TopStruct of TOP-REAL n = TopSpaceMetr Euclid n by EUCLID:def 8; G1 is open by A11,TOPMETR:21,TOPS_3:76; then consider W1 being Subset of T such that A12: p in W1 & W1 is open & f.:W1 c= G1 by A10,JGRAPH_2:20; reconsider r02 = g.p as Point of Euclid n by EUCLID:71; reconsider G2 = Ball(r02,r0/2) as Subset of TOP-REAL n by EUCLID:71; A13: g.p in G2 by A9,GOBOARD6:4; G2 is open by A11,TOPMETR:21,TOPS_3:76; then consider W2 being Subset of T such that A14: p in W2 & W2 is open & g.:W2 c= G2 by A13,JGRAPH_2:20; take W = W1 /\ W2; thus p in W by A12,A14,XBOOLE_0:def 4; thus W is open by A12,A14; let x be Element of TOP-REAL n; assume x in h.:W; then consider z being set such that A15: z in dom h & z in W & h.z=x by FUNCT_1:def 12; A16: z in W1 by A15,XBOOLE_0:def 4; reconsider pz=z as Point of T by A15; dom f=the carrier of T by FUNCT_2:def 1; then A17: f.pz in f.:W1 by A16,FUNCT_1:def 12; reconsider bb1=f.pz as Point of Euclid n by EUCLID:71; dist(r01,bb1)g -> continuous Function of T,TOP-REAL n; coherence proof A26: f <##> g = TIMES(n).:(f,g) by Th54; <:f,g:> is continuous Function of T,[:TOP-REAL n,TOP-REAL n:] by YELLOW12:41; hence thesis by A26; end; end; registration let n,T; let f be continuous Function of T,TOP-REAL n; let g be continuous Function of T,R^1; set I = incl(g,n); cluster f<+>g -> continuous Function of T,TOP-REAL n; coherence proof let h be Function of T,TOP-REAL n; assume A1: h = f<+>g; reconsider G = f<++>I as Function of T,TOP-REAL n by Th39; h = G by A1,Th49; hence thesis; end; cluster f<->g -> continuous Function of T,TOP-REAL n; coherence proof let h be Function of T,TOP-REAL n; assume A2: h = f<->g; reconsider G = f<-->I as Function of T,TOP-REAL n by Th40; h = G by A2,Th50; hence thesis; end; cluster f<#>g -> continuous Function of T,TOP-REAL n; coherence proof let h be Function of T,TOP-REAL n; assume A3: h = f<#>g; reconsider G = f<##>I as Function of T,TOP-REAL n by Th41; h = G by A3,Th51; hence thesis; end; end; registration let n,T; let f be continuous Function of T,TOP-REAL n; let g be non-empty continuous Function of T,R^1; cluster fg -> continuous Function of T,TOP-REAL n; coherence proof let h be Function of T,TOP-REAL n; reconsider g1 = g" as Function of T,R^1; g1 is continuous; hence thesis; end; end; registration let n,T,r; let f be continuous Function of T,TOP-REAL n; cluster f[+]r -> continuous Function of T,TOP-REAL n; coherence proof let h be Function of T,TOP-REAL n such that A1: h = f[+]r; reconsider r as Element of R^1 by XREAL_0:def 1; dom f = the carrier of T by FUNCT_2:def 1; then h = f<+>(T-->r) by A1,Th29; hence thesis; end; cluster f[-]r -> continuous Function of T,TOP-REAL n; coherence; cluster f[#]r -> continuous Function of T,TOP-REAL n; coherence proof let h be Function of T,TOP-REAL n such that A2: h = f[#]r; reconsider r as Element of R^1 by XREAL_0:def 1; dom f = the carrier of T by FUNCT_2:def 1; then h = f<#>(T-->r) by A2,Th31; hence thesis; end; cluster f[/]r -> continuous Function of T,TOP-REAL n; coherence; end; theorem Th60: for r being non negative (real number) for n being non zero Nat, p being Point of Tcircle(0.TOP-REAL n,r) holds -p is Point of Tcircle(0.TOP-REAL n,r) proof let r be non negative (real number); let n be non zero Nat; let p be Point of Tcircle(0.TOP-REAL n,r); reconsider p1 = p as Point of TOP-REAL n by PRE_TOPC:55; A1: n in NAT by ORDINAL1:def 13; then A2: the carrier of Tcircle(0.TOP-REAL n,r) = Sphere(0.TOP-REAL n,r) by TOPREALB:9; |. (-p1) - 0.TOP-REAL n .| = |. -p1 .| by RLVECT_1:26 .= |. p1 .| by EUCLID:75 .= |. p1 - 0.TOP-REAL n .| by RLVECT_1:26 .= r by A1,A2,TOPREAL9:9; hence thesis by A2,A1,TOPREAL9:9; end; theorem Th61: for r being non negative (real number) for f being Function of Tcircle(0.TOP-REAL(n+1),r),TOP-REAL n holds f(-) is Function of Tcircle(0.TOP-REAL(n+1),r),TOP-REAL n proof let r be non negative (real number); set X = the carrier of Tcircle(0.TOP-REAL(n+1),r); let f be Function of X,TOP-REAL n; set g = f(-); A1: dom g = dom f by VALUED_2:def 34; A2: dom f = X by FUNCT_2:def 1; for x st x in X holds g.x in the carrier of TOP-REAL n proof let x; assume x in X; then reconsider x as Element of X; reconsider y = -x as Element of X by Th60; reconsider f as Function of X,TOP-REAL n; g.x = f.y by A1,A2,VALUED_2:def 34; hence thesis; end; hence thesis by A1,A2,FUNCT_2:5; end; definition let n be Nat, r be non negative (real number); let X be Subset of Tcircle(0.TOP-REAL(n+1),r); redefine func (-)X -> Subset of Tcircle(0.TOP-REAL(n+1),r); coherence proof set T = Tcircle(0.TOP-REAL(n+1),r); (-)X c= the carrier of T proof let x; assume A1: x in (-)X; then reconsider x as Element of (-)X; -x in X by A1,Th24; then --x is Point of T by Th60; hence thesis; end; hence thesis; end; end; registration let m; let r be non negative (real number); let X be open Subset of Tcircle(0.TOP-REAL(m+1),r); cluster (-)X -> open Subset of Tcircle(0.TOP-REAL(m+1),r); coherence proof set T = Tcircle(0.TOP-REAL(m+1),r); ex G being Subset of TOP-REAL(m+1) st G is open & (-)X = G /\ the carrier of T proof consider G being Subset of TOP-REAL(m+1) such that A1: G is open and A2: X = G /\ the carrier of T by TSP_1:def 1; take (-)G; thus (-)G is open by A1; thus (-)X c= ((-)G) /\ the carrier of T proof let x; assume A3: x in (-)X; then reconsider x as Element of (-)X; -x in X by A3,Th24; then -x in G by A2,XBOOLE_0:def 4; then x in (-)G by Th24; hence thesis by A3,XBOOLE_0:def 4; end; let x; assume A4: x in ((-)G) /\ the carrier of T; then reconsider x as Element of (-)G by XBOOLE_0:def 4; x in (-)G by A4,XBOOLE_0:def 4; then A5: -x in G by Th24; x in the carrier of T by A4,XBOOLE_0:def 4; then -x is Point of T by Th60; then -x in X by A2,A5,XBOOLE_0:def 4; hence thesis by Th24; end; hence thesis by TSP_1:def 1; end; end; theorem for r being non negative (real number) for f being continuous Function of Tcircle(0.TOP-REAL(m+1),r),TOP-REAL m holds f(-) is continuous Function of Tcircle(0.TOP-REAL(m+1),r),TOP-REAL m proof let r be non negative (real number); set T = Tcircle(0.TOP-REAL(m+1),r); let f be continuous Function of T,TOP-REAL m; reconsider g = f(-) as Function of T,TOP-REAL m by Th61; for p being Point of T, r being positive (real number) ex W being open Subset of T st p in W & g.:W c= Ball(g.p,r) proof let p be Point of T; let r be positive (real number); reconsider q = -p as Point of T by Th60; consider W being open Subset of T such that A1: q in W and A2: f.:W c= Ball(f.q,r) by TOPS_4:18; reconsider W1 = (-)W as open Subset of T; take W1; -q in W1 by A1,Def3; hence p in W1; let y be Element of TOP-REAL m; assume y in g.:W1; then consider x being Element of T such that A3: x in W1 and A4: g.x = y by FUNCT_2:116; dom g = the carrier of T by FUNCT_2:def 1; then A5: g.x = f.-x & g.p = f.-p by VALUED_2:def 34; -x in (-)W1 by A3,Def3; then f.-x in f.:W by FUNCT_2:43; hence y in Ball(g.p,r) by A2,A4,A5; end; hence thesis by TOPS_4:18; end;