toprealc.miz



    begin

    reserve x for object,

X for set,

i,n,m for Nat,

r,s for Real,

c,c1,c2,d for Complex,

f,g for complex-valued Function,

g1 for n -element complex-valued FinSequence,

f1 for n -element real-valued FinSequence,

T for non empty TopSpace,

p for Element of ( TOP-REAL n);

    theorem :: TOPREALC:1

    for X be trivial set, Y be 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 NAT_D: 60;

      

       A3: Y is finite by A1, CARD_1: 38;

      ( card X) = ( card Y) by A1, CARD_1: 5;

      hence thesis by A2, A3, NAT_D: 60;

    end;

    registration

      let r be Real;

      cluster (r ^2 ) -> non negative;

      coherence ;

    end

    registration

      let r be positive Real;

      cluster (r ^2 ) -> positive;

      coherence ;

    end

    registration

      cluster ( sqrt 0 ) -> zero;

      coherence by SQUARE_1: 17;

    end

    registration

      let f be empty set;

      cluster ( sqr f) -> empty;

      coherence ;

      cluster |.f.| -> zero;

      coherence by RVSUM_1: 72;

    end

    theorem :: TOPREALC:2

    

     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 be object;

      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 :: TOPREALC:3

    (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 :: TOPREALC:4

    

     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 be object;

      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 :: TOPREALC:5

    ((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 :: TOPREALC:6

    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 be object;

      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: 130

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

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

      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: 89

      .= (((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 :: TOPREALC:8

    ((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 object;

      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 :: TOPREALC:9

    ((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 object;

      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 :: TOPREALC:10

    ((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 object;

      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: 76

      .= (((f ^2 ) . x) / (c ^2 )) by VALUED_1: 11

      .= (((f ^2 ) (/) (c ^2 )) . x) by VALUED_2: 29;

    end;

    theorem :: TOPREALC:11

    

     Th11: |.((n |-> r) - (n |-> s)).| = (( sqrt n) * |.(r - s).|)

    proof

      

      thus |.((n |-> r) - (n |-> s)).| = ( sqrt ( Sum ( sqr (n |-> (r - s))))) by RVSUM_1: 30

      .= ( sqrt ( Sum (n |-> ((r - s) ^2 )))) by RVSUM_1: 56

      .= ( sqrt (n * ((r - s) ^2 ))) by RVSUM_1: 80

      .= (( sqrt n) * ( sqrt ((r - s) ^2 ))) by SQUARE_1: 29

      .= (( sqrt n) * |.(r - s).|) by COMPLEX1: 72;

    end;

    registration

      let f, x, c;

      cluster (f +* (x,c)) -> complex-valued;

      coherence

      proof

        set F = (f +* (x,c));

        let a be object such that a in ( dom F);

        per cases ;

          suppose x in ( dom f) & x = a;

          hence thesis by FUNCT_7: 31;

        end;

          suppose x in ( dom f) & x <> a;

          then (F . a) = (f . a) by FUNCT_7: 32;

          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 :: TOPREALC:12

    

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

      

       A2: ( dom g) = ( dom ( 0* n)) by FUNCT_7: 30;

      

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

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

        hence thesis by A6, A1, A3, A4, A5, FUNCT_7: 31;

      end;

        suppose

         A7: a <> x;

        

        then

         A8: (f . a) = ((n |-> 0 ) . a) by FUNCT_7: 32

        .= ( {} . x);

        (g . a) = ((n |-> 0 ) . a) by A7, FUNCT_7: 32

        .= ( {} . x);

        hence thesis by A5, A8;

      end;

    end;

    theorem :: TOPREALC:13

    

     Th13: x in ( Seg n) implies |.(( 0* n) +* (x,r)).| = |.r.|

    proof

      set f = (( 0* n) +* (x,r));

      

       A1: n in NAT by ORDINAL1:def 12;

      assume

       A2: x in ( Seg n);

      (f ^2 ) = (( 0* n) +* (x,(r ^2 ))) by Th12;

      then ( Sum (f ^2 )) = (r ^2 ) by A2, A1, JORDAN2B: 10;

      hence thesis by COMPLEX1: 72;

    end;

    theorem :: TOPREALC:14

    

     Th14: (( 0.REAL n) +* (x, 0 )) = ( 0.REAL n)

    proof

      set p = (( 0.REAL n) +* (x, 0 ));

      

       A1: ( dom p) = ( Seg n) by FINSEQ_1: 89;

      

       A2: ( dom (( 0.REAL n) +* (x, 0 ))) = ( dom ( 0.REAL n)) by FUNCT_7: 30;

      

       A3: ( dom ( 0.REAL n)) = ( Seg n);

      now

        let z be object;

        assume

         A4: z in ( dom p);

        per cases ;

          suppose z = x;

          

          hence (p . z) = 0 by A1, A3, A4, FUNCT_7: 31

          .= (( 0.REAL n) . z);

        end;

          suppose z <> x;

          hence (p . z) = (( 0.REAL n) . z) by FUNCT_7: 32;

        end;

      end;

      hence thesis by A2;

    end;

    theorem :: TOPREALC:15

    

     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 FINSEQ_1: 89;

      

       A2: ( dom p) = ( Seg n) by FINSEQ_1: 89;

      

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

      

       A5: ( dom ( 0.REAL n)) = ( Seg n);

      now

        let z be object;

        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: 31

          .= ((( 0.REAL n) +* (x,((f1 . x) * r))) . z) by A1, A2, A3, A5, A6, A8, FUNCT_7: 31;

        end;

          suppose

           A9: z <> x;

          

          hence (( mlt (f1,p)) . z) = ((f1 . z) * (( 0.REAL n) . z)) by A7, FUNCT_7: 32

          .= ((f1 . z) * ((n |-> 0 ) . z))

          .= ((( 0.REAL n) +* (x,((f1 . x) * r))) . z) by A9, FUNCT_7: 32;

        end;

      end;

      hence thesis by A4, FINSEQ_1: 89;

    end;

    theorem :: TOPREALC:16

     |(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 FINSEQ_1: 89;

      

       A3: n in NAT by ORDINAL1:def 12;

      per cases ;

        suppose x in ( dom f1);

        hence thesis by A1, A2, A3, JORDAN2B: 10;

      end;

        suppose not x in ( dom f1);

        then

         A4: (f1 . x) = 0 by FUNCT_1:def 2;

        

        hence |(f1, (( 0.REAL n) +* (x,r)))| = ( Sum ( 0.REAL n)) by A1, Th14

        .= ((f1 . x) * r) by A4, A3, JORDAN2B: 9;

      end;

    end;

    theorem :: TOPREALC:17

    

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

      

       A3: ( dom g1) = ( Seg n) by FINSEQ_1: 89;

      

       A4: ( dom (g1 +* (i,c))) = ( dom g1) by FUNCT_7: 30;

      hence ( dom ((g1 +* (i,c)) - g1)) = ( dom (( 0* n) +* (i,(c - (g1 . i))))) by A1, A3, FINSEQ_1: 89;

      let x be object;

      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: 31

        .= ((( 0* n) +* (i,(c - (g1 . i)))) . x) by A1, A2, A3, A5, A4, A7, FUNCT_7: 31;

      end;

        suppose

         A8: x <> i;

        

        hence (((g1 +* (i,c)) - g1) . x) = ((g1 . x) - (g1 . x)) by A6, FUNCT_7: 32

        .= ((n |-> 0 ) . x)

        .= ((( 0* n) +* (i,(c - (g1 . i)))) . x) by A8, FUNCT_7: 32;

      end;

    end;

    theorem :: TOPREALC:18

     |. <*r*>.| = |.r.|

    proof

      set f = <*r*>;

      ( sqr f) = <*(r ^2 )*> by RVSUM_1: 55;

      then ( Sum ( sqr f)) = (r ^2 ) by RVSUM_1: 73;

      hence thesis by COMPLEX1: 72;

    end;

    theorem :: TOPREALC:19

    for f be real-valued FinSequence holds f is FinSequence of REAL by RVSUM_1: 145;

    theorem :: TOPREALC:20

    for f be real-valued FinSequence st |.f.| <> 0 holds ex i be Nat st i in ( dom f) & (f . i) <> 0

    proof

      let f be real-valued FinSequence;

      assume |.f.| <> 0 ;

      then

      consider i be Element of NAT such that

       A1: i in ( dom ( sqr f)) and

       A2: (( sqr f) . i) <> 0 by PRVECT_2: 3, SQUARE_1: 17;

      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 :: TOPREALC:21

    

     Th21: for f be real-valued FinSequence holds |.( Sum f).| <= ( Sum ( abs f))

    proof

      let f be real-valued FinSequence;

      defpred P[ set] means ex F be real-valued FinSequence st F = $1 & |.( Sum F).| <= ( Sum ( abs F));

      

       A1: P[( <*> REAL )]

      proof

        take ( <*> REAL );

        thus thesis by ABSVALUE: 2, RVSUM_1: 72;

      end;

      

       A2: for p be FinSequence of REAL , x be Element of REAL st P[p] holds P[(p ^ <*x*>)]

      proof

        let p be FinSequence of REAL , x be Element of REAL ;

        given F be real-valued FinSequence such that

         A3: F = p and

         A4: |.( Sum F).| <= ( Sum ( abs F));

        

         A5: ( |.( Sum F).| + |.x.|) <= (( Sum ( abs F)) + |.x.|) by A4, XREAL_1: 6;

        take G = (p ^ <*x*>);

        

         A6: ( abs <*x*>) = <* |.x.|*> by JORDAN2B: 19;

        

         A7: ( Sum <* |.x.|*>) = |.x.| by RVSUM_1: 73;

        ( abs G) = (( abs p) ^ ( abs <*x*>)) by TOPREAL7: 11;

        then

         A8: ( Sum ( abs G)) = (( Sum ( abs p)) + |.x.|) by A6, A7, RVSUM_1: 75;

        ( Sum G) = (( Sum p) + x) by RVSUM_1: 74;

        then |.( Sum G).| <= ( |.( Sum p).| + |.x.|) by COMPLEX1: 56;

        hence thesis by A8, A3, A5, XXREAL_0: 2;

      end;

      

       A9: for p be FinSequence of REAL holds P[p] from FINSEQ_2:sch 2( A1, A2);

      f is FinSequence of REAL by RVSUM_1: 145;

      then P[f] by A9;

      hence thesis;

    end;

    theorem :: TOPREALC:22

    for A be non empty 1-sorted, B be 1 -element 1-sorted holds for t be Point of B holds for f be Function of A, B holds f = (A --> t)

    proof

      let A be non empty 1-sorted;

      let B be 1 -element 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 ;

    end

    definition

      let n;

      let p be Element of ( REAL n);

      let r;

      :: original: (/)

      redefine

      func p (/) r -> Element of ( REAL n) ;

      coherence

      proof

        

         A1: (p (/) r) is FinSequence of REAL by RVSUM_1: 145;

        

         A2: ( len p) = n by CARD_1:def 7;

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

        hence thesis by A1, FINSEQ_2: 92;

      end;

    end

    theorem :: TOPREALC:23

    

     Th23: for p,q be 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:

      now

        let a,b be Point of ( TOP-REAL m);

        assume a in ( Ball (b,r));

        then

         A2: |.(a - b).| < r by TOPREAL9: 7;

        (( - a) - ( - b)) = (( - a) + ( - ( - b)))

        .= ( - (a - b)) by RLVECT_1: 31;

        then |.(( - a) - ( - b)).| = |.(a - b).| by EUCLID: 71;

        hence ( - a) in ( Ball (( - b),r)) by A2, TOPREAL9: 7;

      end;

      ( - ( - p)) = p & ( - ( - q)) = q;

      hence thesis by A1;

    end;

    definition

      let S be 1-sorted;

      :: TOPREALC:def1

      attr S is complex-functions-membered means

      : Def1: the carrier of S is complex-functions-membered;

      :: TOPREALC:def2

      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 by EUCLID: 22, EUCLID: 77;

    end

    registration

      cluster ( TOP-REAL 0 ) -> trivial;

      coherence ;

    end

    registration

      cluster real-functions-membered -> complex-functions-membered for 1-sorted;

      coherence ;

    end

    registration

      cluster strict non empty real-functions-membered for 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 for TopSpace;

      existence

      proof

        take the TopStruct of ( TOP-REAL 1);

        thus thesis;

      end;

    end

    registration

      let S be complex-functions-membered TopSpace;

      cluster -> complex-functions-membered for 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: 1;

        hence thesis;

      end;

    end

    registration

      let S be real-functions-membered TopSpace;

      cluster -> real-functions-membered for 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: 1;

        hence thesis;

      end;

    end

    definition

      let X be complex-functions-membered set;

      :: TOPREALC:def3

      func (-) X -> complex-functions-membered set means

      : Def3: for f be complex-valued Function holds ( - f) in it iff f in X;

      existence

      proof

        set F = { ( - f) where f be Element of X : f in X };

        F is complex-functions-membered

        proof

          let x;

          assume x in F;

          then ex f be 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 be Element of X st ( - f) = ( - g) & g in X;

          hence f in X by RVSUM_1: 24;

        end;

        thus thesis;

      end;

      uniqueness

      proof

        let A,B be complex-functions-membered set such that

         A1: for f be complex-valued Function holds ( - f) in A iff f in X and

         A2: for f be complex-valued Function holds ( - f) in B iff f in X;

        thus A c= B

        proof

          let x be object;

          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 be object;

        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 be 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 be object such that

         A1: x in ( (-) X);

        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 be object 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 :: TOPREALC:24

    

     Th24: for X be complex-functions-membered set, f be 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 :: TOPREALC:25

    

     Th25: for X be Subset of ( TOP-REAL n) holds ( - X) = ( (-) X)

    proof

      set T = ( TOP-REAL n);

      let X be Subset of T;

      for f be 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 be 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

          .= v;

          hence f in X by A2;

        end;

        assume

         A3: f in X;

        then

        reconsider g = f as Element of T;

        ( - g) = (( - 1) * g);

        hence thesis by A3;

      end;

      hence thesis by Def3;

    end;

    definition

      let n;

      let X be Subset of ( TOP-REAL n);

      :: original: (-)

      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;

      coherence

      proof

        reconsider n as Element of NAT by ORDINAL1:def 12;

        reconsider Y = ( (-) X) as Subset of ( TOP-REAL n);

        for p be Point of ( TOP-REAL n) st p in Y holds ex r be positive Real 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 be positive Real 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 R,S,T be non empty TopSpace, f be Function of [:R, S:], T;

      let x be Point of [:R, S:];

      :: original: .

      redefine

      func f . x -> Point of T ;

      coherence

      proof

        consider x1 be Point of R, x2 be Point of S such that

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

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

      :: original: .

      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;

      :: original: +

      redefine

      func p + r -> Point of ( TOP-REAL n) ;

      coherence

      proof

        

         A1: (p + r) is FinSequence of REAL by RVSUM_1: 145;

        

         A2: ( len p) = n by CARD_1:def 7;

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

        then (p + r) is Element of ( REAL n) by A1, FINSEQ_2: 92;

        hence thesis by EUCLID: 22;

      end;

    end

    definition

      let n, p, r;

      :: original: -

      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;

      :: original: (#)

      redefine

      func p (#) r -> Point of ( TOP-REAL n) ;

      coherence

      proof

        

         A1: (p (#) r) is FinSequence of REAL by RVSUM_1: 145;

        

         A2: ( len p) = n by CARD_1:def 7;

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

        then (p (#) r) is Element of ( REAL n) by A1, FINSEQ_2: 92;

        hence thesis by EUCLID: 22;

      end;

    end

    definition

      let n, p, r;

      :: original: (/)

      redefine

      func p (/) r -> Point of ( TOP-REAL n) ;

      coherence

      proof

        reconsider f = p as Element of ( REAL n) by EUCLID: 22;

        (f (/) r) is Element of ( REAL n);

        hence thesis by EUCLID: 22;

      end;

    end

    definition

      let n;

      let p1,p2 be Point of ( TOP-REAL n);

      :: original: (#)

      redefine

      func p1 (#) p2 -> Point of ( TOP-REAL n) ;

      coherence

      proof

        

         A1: (p1 (#) p2) is FinSequence of REAL by RVSUM_1: 145;

        

         A2: ( len p1) = n & ( len p2) = n by CARD_1:def 7;

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

        then (p1 (#) p2) is Element of ( REAL n) by A1, FINSEQ_2: 92;

        hence thesis by EUCLID: 22;

      end;

    end

    definition

      let n;

      let p be Point of ( TOP-REAL n);

      :: original: sqr

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

      :: original: /"

      redefine

      func p1 /" p2 -> Point of ( TOP-REAL n) ;

      coherence

      proof

        

         A1: (p1 /" p2) is FinSequence of REAL by RVSUM_1: 145;

        

         A2: ( len p1) = n & ( len p2) = n by CARD_1:def 7;

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

        then (p1 /" p2) is Element of ( REAL n) by A1, FINSEQ_2: 92;

        hence thesis by EUCLID: 22;

      end;

    end

    definition

      let n, p, x, r;

      :: original: +*

      redefine

      func p +* (x,r) -> Point of ( TOP-REAL n) ;

      coherence

      proof

        

         A1: (p +* (x,r)) is FinSequence of REAL by RVSUM_1: 145;

        

         A2: ( len p) = n by CARD_1:def 7;

        ( Seg ( len (p +* (x,r)))) = ( dom (p +* (x,r))) by FINSEQ_1:def 3

        .= ( dom p) by FUNCT_7: 30

        .= ( Seg n) by A2, FINSEQ_1:def 3;

        then ( len (p +* (x,r))) = n by FINSEQ_1: 6;

        then (p +* (x,r)) is Element of ( REAL n) by A1, FINSEQ_2: 92;

        hence thesis by EUCLID: 22;

      end;

    end

    theorem :: TOPREALC:26

    for a,o be Point of ( TOP-REAL n) holds n <> 0 & a in ( Ball (o,r)) implies |.( 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: 80;

      

       A5: for j be 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: 57;

         |.(R1 . j).| < r by A2, EUCLID_9: 9;

        hence thesis by A6, VALUED_1: 18;

      end;

      then

       A7: for j be Nat st j in ( Seg n) holds (( abs R1) . j) <= (R2 . j);

      ex j be 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, RVSUM_1: 83;

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

    end

    theorem :: TOPREALC:27

    for V be add-associative right_zeroed right_complementable non empty addLoopStr, v,u be 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: 28

      .= (v + ( 0. V)) by RLVECT_1: 5

      .= v;

    end;

    theorem :: TOPREALC:28

    for V be Abelian add-associative right_zeroed right_complementable non empty addLoopStr, v,u be 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: 29

      .= (v - ( 0. V)) by RLVECT_1: 5

      .= v;

    end;

    theorem :: TOPREALC:29

    

     Th29: for Y be complex-functions-membered set, f be 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;

      now

        let x be object;

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

        .= ((f <+> g) . x) by A1, A2, A4, VALUED_2:def 41;

      end;

      hence thesis by A1, A2;

    end;

    theorem :: TOPREALC:30

    for Y be complex-functions-membered set, f be 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;

      now

        let x be object;

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

        .= ((f <-> g) . x) by A1, A2, A4, VALUED_2: 62;

      end;

      hence thesis by A1, A2;

    end;

    theorem :: TOPREALC:31

    

     Th31: for Y be complex-functions-membered set, f be 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;

      now

        let x be object;

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

        .= ((f <#> g) . x) by A1, A2, A4, VALUED_2:def 43;

      end;

      hence thesis by A1, A2;

    end;

    theorem :: TOPREALC:32

    for Y be complex-functions-membered set, f be 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: 71;

      now

        let x be object;

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

        .= ((f </> g) . x) by A1, A2, A4, VALUED_2: 72;

      end;

      hence thesis by A1, A2;

    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 (f <//> g) -> FinSequence-like;

      coherence

      proof

        ( dom (f <//> g)) = (( dom f) /\ ( dom g)) by VALUED_2:def 48;

        hence thesis by VALUED_1: 19;

      end;

    end

    theorem :: TOPREALC:33

    for f be 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: 3;

    end;

    theorem :: TOPREALC:34

    

     Th34: for f be 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: 3;

    end;

    theorem :: TOPREALC:35

    

     Th35: for f be 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: 3;

    end;

    theorem :: TOPREALC:36

    for f be Function of X, ( TOP-REAL n) holds (f [-] r) is Function of X, ( TOP-REAL n) by Th35;

    theorem :: TOPREALC:37

    

     Th37: for f be 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: 3;

    end;

    theorem :: TOPREALC:38

    for f be Function of X, ( TOP-REAL n) holds (f [/] r) is Function of X, ( TOP-REAL n) by Th37;

    theorem :: TOPREALC:39

    

     Th39: for f,g be 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: 3;

    end;

    theorem :: TOPREALC:40

    

     Th40: for f,g be 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: 3;

    end;

    theorem :: TOPREALC:41

    

     Th41: for f,g be 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: 3;

    end;

    theorem :: TOPREALC:42

    

     Th42: for f,g be 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 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: 3;

    end;

    theorem :: TOPREALC:43

    

     Th43: for f be Function of X, ( TOP-REAL n), g be 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: 3;

    end;

    theorem :: TOPREALC:44

    

     Th44: for f be Function of X, ( TOP-REAL n), g be 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: 3;

    end;

    theorem :: TOPREALC:45

    

     Th45: for f be Function of X, ( TOP-REAL n), g be 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: 3;

    end;

    theorem :: TOPREALC:46

    

     Th46: for f be Function of X, ( TOP-REAL n), g be 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: 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: 3;

    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;

      :: TOPREALC:def4

      func incl (f,n) -> Function of T, ( TOP-REAL n) means

      : Def4: for t be Element of T holds (it . t) = (n |-> (f . t));

      existence

      proof

        defpred P[ set, set] means $2 = (n |-> (f . $1));

        

         A1: for x be Element of T holds ex y be 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: 112;

          then

          reconsider y = (n |-> (f . x)) as Point of ( TOP-REAL n) by EUCLID: 22;

          take y;

          thus thesis;

        end;

        ex F be Function of T, ( TOP-REAL n) st for x be 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 be Element of T holds (F . t) = (n |-> (f . t)) and

         A3: for t be 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 :: TOPREALC:47

    

     Th47: for R be real-membered set holds for f be Function of T, R, t be 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: 57;

    end;

    theorem :: TOPREALC:48

    

     Th48: for T be non empty set, R be real-membered set, f be 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 :: TOPREALC:49

    

     Th49: for f be Function of T, ( TOP-REAL n), g be 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 FINSEQ_1: 89;

          

           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, FINSEQ_1: 89;

          let x be object;

          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 :: TOPREALC:50

    

     Th50: for f be Function of T, ( TOP-REAL n), g be 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 FINSEQ_1: 89;

          

           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, FINSEQ_1: 89;

          let x be object;

          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 :: TOPREALC:51

    

     Th51: for f be Function of T, ( TOP-REAL n), g be 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 FINSEQ_1: 89;

          

           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 FINSEQ_1: 89;

          let x be object;

          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 :: TOPREALC:52

    for f be Function of T, ( TOP-REAL n), g be 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 Th46;

      reconsider G = (f <//> I) 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 FINSEQ_1: 89;

          

           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 FINSEQ_1: 89;

          let x be object;

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

      :: TOPREALC:def5

      func TIMES (n) -> Function of [:( TOP-REAL n), ( TOP-REAL n):], ( TOP-REAL n) means

      : Def5: for x,y be 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 be Function of [:c, c:], c st for x,y be 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 be Point of T holds (f . (x,y)) = (x (#) y) and

         A3: for x,y be 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 :: TOPREALC:53

    

     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 :: TOPREALC:54

    

     Th54: for f,g be 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 2;

      then [:( rng f), ( rng g):] c= ( dom F) by ZFMISC_1: 96;

      then

       A2: ( dom (F .: (f,g))) = (( dom f) /\ ( dom g)) by FUNCOP_1: 69;

      now

        let x be object;

        assume

         A3: x in ( dom (f <##> g));

        then

         A4: (f . x) is Point of R & (g . x) is Point of R by FUNCT_2: 5;

        

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

      end;

      hence thesis by A1, A2;

    end;

    definition

      let m, n;

      

       A1: m in NAT & n in NAT by ORDINAL1:def 12;

      :: TOPREALC:def6

      func PROJ (m,n) -> Function of ( TOP-REAL m), R^1 means

      : Def6: for p be 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 be Element of ( TOP-REAL m) holds (F . p) = (p /. n) and

         A3: for p be 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 :: TOPREALC:55

    

     Th55: for p be 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);

      per cases ;

        suppose

         A2: r <= 0 ;

        then ].((p /. n) - r), ((p /. n) + r).[ = {} ;

        hence thesis by A2;

      end;

        suppose

         A3: 0 < r;

        

         A4: ( dom p) = ( Seg m) by FINSEQ_1: 89;

        thus (( PROJ (m,n)) .: ( Ball (p,r))) c= ].((p /. n) - r), ((p /. n) + r).[

        proof

          let y be object;

          assume y in (( PROJ (m,n)) .: ( Ball (p,r)));

          then

          consider x be Element of ( TOP-REAL m) such that

           A5: x in ( Ball (p,r)) and

           A6: y = (( PROJ (m,n)) . x) by FUNCT_2: 65;

          

           A7: (( PROJ (m,n)) . x) = (x /. n) by Def6;

          

           A8: |.(x - p).| < r by A5, TOPREAL9: 7;

           0 <= ( Sum ( sqr (x - p))) by RVSUM_1: 86;

          then (( sqrt ( Sum ( sqr (x - p)))) ^2 ) = ( Sum ( sqr (x - p))) by SQUARE_1:def 2;

          then

           A9: ( Sum ( sqr (x - p))) < (r ^2 ) by A8, SQUARE_1: 16;

          ( dom x) = ( Seg m) by FINSEQ_1: 89;

          then (((x /. n) - (p /. n)) ^2 ) <= ( Sum ( sqr (x - p))) by A4, A1, EUCLID_9: 8;

          then (((x /. n) - (p /. n)) ^2 ) < (r ^2 ) by A9, XXREAL_0: 2;

          then ( - r) < ((x /. n) - (p /. n)) & ((x /. n) - (p /. n)) < r by A3, SQUARE_1: 48;

          then (( - r) + (p /. n)) < (((x /. n) - (p /. n)) + (p /. n)) & (((x /. n) - (p /. n)) + (p /. n)) < (r + (p /. n)) by XREAL_1: 6;

          hence thesis by A6, A7, XXREAL_1: 4;

        end;

        let y be object;

        assume

         A10: 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: 24;

        

         A11: ( dom X) = ( dom p) by FUNCT_7: 30;

        

         A12: (p /. n) = (p . n) by A1, PARTFUN1:def 6;

        ((p /. n) - r) < y & y < ((p /. n) + r) by A10, XXREAL_1: 4;

        then

         A13: (y - (p /. n)) < r & ( - r) < (y - (p /. n)) by XREAL_1: 19, XREAL_1: 20;

        (x - p) = (( 0* m) +* (n,(y - (p . n)))) by Th17;

        then |.(x - p).| = |.(y - (p . n)).| by A1, A4, Th13;

        then |.(x - p).| < r by A12, A13, SEQ_2: 1;

        then

         A14: x in ( Ball (p,r)) by TOPREAL9: 7;

        (( PROJ (m,n)) . x) = (x /. n) by Def6

        .= (X . n) by A11, A1, PARTFUN1:def 6

        .= y by A1, FUNCT_7: 31;

        hence thesis by A14, FUNCT_2: 35;

      end;

    end;

    theorem :: TOPREALC:56

    for m be non zero Nat holds for f be 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 ;

      1 <= m by NAT_1: 14;

      then

       A1: m in ( Seg m);

      

       A2: ( dom (m |-> (f . p))) = ( Seg m);

      

      thus ((( PROJ (m,m)) * I) . p) = (( PROJ (m,m)) . (I . p)) by FUNCT_2: 15

      .= ((I . p) /. m) by Def6

      .= (G /. m) by Def4

      .= (G . m) by A1, A2, PARTFUN1:def 6

      .= (f . p) by A1, FINSEQ_2: 57;

    end;

    begin

    registration

      let T;

      cluster non-empty continuous for Function of T, R^1 ;

      existence

      proof

        take (T --> ( R^1 1));

        thus thesis;

      end;

    end

    theorem :: TOPREALC:57

    n in ( Seg m) implies ( PROJ (m,n)) is continuous

    proof

      assume

       A1: n in ( Seg m);

      

       A2: m in NAT by ORDINAL1:def 12;

      for p be Element of ( TOP-REAL m) holds (( PROJ (m,n)) . p) = (p /. n) by Def6;

      hence thesis by A2, A1, JORDAN2B: 18;

    end;

    theorem :: TOPREALC:58

    n in ( Seg m) implies ( PROJ (m,n)) is open

    proof

      set f = ( PROJ (m,n));

      assume

       A1: n in ( Seg m);

      for p be Point of ( TOP-REAL m), r be positive Real holds ex s be positive Real 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;

        take r;

        

         A2: ( dom p) = ( Seg m) by FINSEQ_1: 89;

        (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 12;

        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 be Point of T, V be Subset of ( TOP-REAL n) st (g . p) in V & V is open holds ex W be 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: 23;

            reconsider s = (g . p) as Point of ( Euclid n) by EUCLID: 67;

            consider r be Real such that

             A6: r > 0 and

             A7: ( Ball (s,r)) c= V by A5, GOBOARD6: 5;

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

            

             A9: F = (n |-> (f . p)) by Def4;

            

             A10: ( dom (n |-> (f . p))) = ( Seg n);

            

             A11: ((g . p) /. n) = (G /. n) by Def4

            .= (G . n) by A8, A10, PARTFUN1:def 6

            .= (f . p) by A8, FINSEQ_2: 57;

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

            then

            consider W be Subset of T such that

             A12: p in W & W is open and

             A13: (f .: W) c= RR by JGRAPH_2: 10;

            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 be Element of T such that

             A14: x in W and

             A15: (g . x) = y by FUNCT_2: 65;

            reconsider y1 = y as Point of ( Euclid n) by EUCLID: 67;

            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) * |.((f . x) - (f . p)).|) by A16, A9, Th11;

            (f . x) in (f .: W) by A14, FUNCT_2: 35;

            then |.((f . x) - (f . p)).| < R by A13, A11, RCOMP_1: 1;

            then ( dist (y1,s)) < r by A2, A17, XREAL_1: 79;

            then y in ( Ball (s,r)) by METRIC_1: 11;

            hence thesis by A7;

          end;

          hence thesis by JGRAPH_2: 10;

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

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

          now

            let i be Element of ( Seg n);

            set P = ( proj (J,i));

            reconsider f = (P * F) as Function of [:T, T:], R^1 ;

            

             A5: the carrier of [:T, T:] = [:c, c:] by BORSUK_1:def 2;

            

             A6: for a,b be 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: 18

              .= (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) = ( In (($1 . i), REAL ));

            consider f1 be Function of [:c, c:], REAL such that

             A7: for a,b be 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) = ( In (($2 . i), REAL ));

            consider f2 be Function of [:c, c:], REAL such that

             A8: for a,b be 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 be Point of [:T, T:], r be positive Real holds ex W be 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;

              consider p1,p2 be Point of T such that

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

              set B1 = ( Ball (p1,r)), B2 = ( [#] T);

              reconsider W = [:B1, B2:] as open Subset of [:T, T:] by BORSUK_1: 6;

              take W;

              p1 in B1 & p2 in B2 by TOPGEN_5: 13;

              hence p in W by A9, ZFMISC_1:def 2;

              let y be object;

              assume y in (f1 .: W);

              then

              consider x be Point of [:T, T:] such that

               A10: x in W and

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

              consider x1,x2 be Point of T such that

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

              

               A13: (f1 . (x1,x2)) = F1(x1,x2) & (f1 . (p1,p2)) = F1(p1,p2) by A7;

              x1 in B1 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;

            end;

            then

             A15: f1 is continuous by TOPS_4: 21;

            for p be Point of [:T, T:], r be positive Real holds ex W be 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;

              consider p1,p2 be Point of T such that

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

              set B1 = ( [#] T), B2 = ( Ball (p2,r));

              reconsider W = [:B1, B2:] as open Subset of [:T, T:] by BORSUK_1: 6;

              take W;

              p1 in B1 & p2 in B2 by TOPGEN_5: 13;

              hence p in W by A16, ZFMISC_1:def 2;

              let y be object;

              assume y in (f2 .: W);

              then

              consider x be Point of [:T, T:] such that

               A17: x in W and

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

              consider x1,x2 be Point of T such that

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

              

               A20: (f2 . (x1,x2)) = F2(x1,x2) & (f2 . (p1,p2)) = F2(p1,p2) by A8;

              x2 in B2 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;

            end;

            then f2 is continuous by TOPS_4: 21;

            then

            consider g be Function of [:T, T:], R^1 such that

             A22: for p be Point of [:T, T:], r1,r2 be Real st (f1 . p) = r1 & (f2 . p) = r2 holds (g . p) = (r1 * r2) and

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

            now

              let a,b be Point of T;

              

               A24: (f1 . (a,b)) = F1(a,b) & (f2 . (a,b)) = F2(a,b) 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, A5, BINOP_1: 2;

          end;

          then F is continuous by WAYBEL18: 6;

          hence thesis by A1, A2, YELLOW12: 36;

        end;

          suppose n is zero;

          then n = 0 ;

          hence thesis by Th53;

        end;

      end;

    end

    theorem :: TOPREALC:59

    for f be 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 be Point of ( TOP-REAL m), r be positive Real holds ex s be positive Real st (g .: ( Ball (p,s))) c= ( Ball ((g . p),r))

      proof

        let p be Point of ( TOP-REAL m);

        let r be positive Real;

        consider s be positive Real 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 be Element of ( TOP-REAL m) such that

         A3: x in ( Ball (p,s)) and

         A4: (g . x) = y by FUNCT_2: 65;

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

        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;

      coherence

      proof

        let F be Function of T, R^1 such that

         A1: F = ( - f);

        consider g be Function of T, R^1 such that

         A2: for p be Point of T, r be Real st (f . p) = r holds (g . p) = ( - r) and

         A3: g is continuous by JGRAPH_4: 8;

        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;

      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 be Point of T holds (f . q) <> 0 ;

        then

        consider g be Function of T, R^1 such that

         A2: for p be Point of T, r be Real st (f . p) = r holds (g . p) = (1 / r) and

         A3: g is continuous by JGRAPH_2: 26;

        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;

      coherence

      proof

        let F be Function of T, R^1 such that

         A1: F = (f + r);

        consider g be Function of T, R^1 such that

         A2: for p be Point of T, s be Real st (f . p) = s holds (g . p) = (s + r) and

         A3: g is continuous by JGRAPH_2: 24;

        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;

      coherence ;

      cluster (f (#) r) -> continuous;

      coherence

      proof

        let F be Function of T, R^1 such that

         A4: F = (f (#) r);

        consider g be Function of T, R^1 such that

         A5: for p be Point of T, s be Real st (f . p) = s holds (g . p) = (r * s) and

         A6: g is continuous by JGRAPH_2: 23;

        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;

      coherence ;

    end

    registration

      let T;

      let f,g be continuous Function of T, R^1 ;

      cluster (f + g) -> continuous;

      coherence

      proof

        let F be Function of T, R^1 such that

         A1: F = (f + g);

        consider h be Function of T, R^1 such that

         A2: for p be Point of T, r1,r2 be Real st (f . p) = r1 & (g . p) = r2 holds (h . p) = (r1 + r2) and

         A3: h is continuous by JGRAPH_2: 19;

        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;

      coherence

      proof

        (f - g) = (f + ( - g));

        hence thesis;

      end;

      cluster (f (#) g) -> continuous;

      coherence

      proof

        let F be Function of T, R^1 such that

         A4: F = (f (#) g);

        consider h be Function of T, R^1 such that

         A5: for p be Point of T, r1,r2 be Real st (f . p) = r1 & (g . p) = r2 holds (h . p) = (r1 * r2) and

         A6: h is continuous by JGRAPH_2: 25;

        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;

      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;

      coherence

      proof

        let h be Function of T, ( TOP-REAL n) such that

         A1: h = (f <++> g);

        consider F be Function of T, ( TOP-REAL n) such that

         A2: for r be Point of T holds (F . r) = ((f . r) + (g . r)) and

         A3: F is continuous by JGRAPH_6: 12;

        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;

      coherence

      proof

        let h be Function of T, ( TOP-REAL n) such that

         A5: h = (f <--> g);

        

         A6: for r be 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 be Point of T, V be Subset of ( TOP-REAL n) st (h . p) in V & V is open holds ex W be 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

           A7: (h . p) in ( Int V) by TOPS_1: 23;

          reconsider r = (h . p) as Point of ( Euclid n) by EUCLID: 67;

          consider r0 be Real such that

           A8: r0 > 0 & ( Ball (r,r0)) c= V by A7, GOBOARD6: 5;

          reconsider r01 = (f . p) as Point of ( Euclid n) by EUCLID: 67;

          reconsider G1 = ( Ball (r01,(r0 / 2))) as Subset of ( TOP-REAL n) by EUCLID: 67;

          

           A9: (f . p) in G1 by A8, GOBOARD6: 1;

          

           A10: the TopStruct of ( TOP-REAL n) = ( TopSpaceMetr ( Euclid n)) by EUCLID:def 8;

          G1 is open by A10, TOPMETR: 14, TOPS_3: 76;

          then

          consider W1 be Subset of T such that

           A11: p in W1 & W1 is open & (f .: W1) c= G1 by A9, JGRAPH_2: 10;

          reconsider r02 = (g . p) as Point of ( Euclid n) by EUCLID: 67;

          reconsider G2 = ( Ball (r02,(r0 / 2))) as Subset of ( TOP-REAL n) by EUCLID: 67;

          

           A12: (g . p) in G2 by A8, GOBOARD6: 1;

          G2 is open by A10, TOPMETR: 14, TOPS_3: 76;

          then

          consider W2 be Subset of T such that

           A13: p in W2 & W2 is open & (g .: W2) c= G2 by A12, JGRAPH_2: 10;

          take W = (W1 /\ W2);

          thus p in W by A11, A13, XBOOLE_0:def 4;

          thus W is open by A11, A13;

          let x be Element of ( TOP-REAL n);

          assume x in (h .: W);

          then

          consider z be object such that

           A14: z in ( dom h) & z in W & (h . z) = x by FUNCT_1:def 6;

          

           A15: z in W1 by A14, XBOOLE_0:def 4;

          reconsider pz = z as Point of T by A14;

          ( dom f) = the carrier of T by FUNCT_2:def 1;

          then

           A16: (f . pz) in (f .: W1) by A15, FUNCT_1:def 6;

          reconsider bb1 = (f . pz) as Point of ( Euclid n) by EUCLID: 67;

          ( dist (r01,bb1)) < (r0 / 2) by A11, A16, METRIC_1: 11;

          then

           A17: |.((f . p) - (f . pz)).| < (r0 / 2) by JGRAPH_1: 28;

          

           A18: z in W2 by A14, XBOOLE_0:def 4;

          ( dom g) = the carrier of T by FUNCT_2:def 1;

          then

           A19: (g . pz) in (g .: W2) by A18, FUNCT_1:def 6;

          reconsider bb2 = (g . pz) as Point of ( Euclid n) by EUCLID: 67;

          ( dist (r02,bb2)) < (r0 / 2) by A13, A19, METRIC_1: 11;

          then

           A20: |.((g . p) - (g . pz)).| < (r0 / 2) by JGRAPH_1: 28;

          

           A21: ((f . pz) - (g . pz)) = x by A6, A14;

          reconsider bb0 = ((f . pz) - (g . pz)) as Point of ( Euclid n) by EUCLID: 67;

          

           A22: (h . pz) = ((f . pz) - (g . pz)) by A6;

          (((f . p) - (g . p)) - ((f . pz) - (g . pz))) = ((((f . p) - (g . p)) - (f . pz)) + (g . pz)) by RLVECT_1: 29

          .= ((((f . p) + ( - (g . p))) + ( - (f . pz))) + (g . pz))

          .= ((((f . p) + ( - (f . pz))) + ( - (g . p))) + (g . pz)) by RLVECT_1:def 3

          .= ((((f . p) - (f . pz)) - (g . p)) + (g . pz))

          .= ((((f . p) - (f . pz)) + (g . pz)) + ( - (g . p))) by RLVECT_1:def 3

          .= (((f . p) - (f . pz)) + ((g . pz) - (g . p))) by RLVECT_1:def 3;

          then

           A23: |.(((f . p) - (g . p)) - ((f . pz) - (g . pz))).| <= ( |.((f . p) - (f . pz)).| + |.((g . pz) - (g . p)).|) by TOPRNS_1: 29;

          

           A24: |.((g . p) - (g . pz)).| = |.( - ((g . pz) - (g . p))).| by RLVECT_1: 33

          .= |.((g . pz) - (g . p)).| by TOPRNS_1: 26;

          ( |.((f . p) - (f . pz)).| + |.((g . p) - (g . pz)).|) < ((r0 / 2) + (r0 / 2)) by A17, A20, XREAL_1: 8;

          then |.(((f . p) - (g . p)) - ((f . pz) - (g . pz))).| < r0 by A23, A24, XXREAL_0: 2;

          then |.((h . p) - (h . pz)).| < r0 by A6, A22;

          then ( dist (r,bb0)) < r0 by A14, A21, JGRAPH_1: 28;

          then x in ( Ball (r,r0)) by A21, METRIC_1: 11;

          hence thesis by A8;

        end;

        hence thesis by JGRAPH_2: 10;

      end;

      cluster (f <##> g) -> continuous;

      coherence

      proof

        

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

      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;

      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;

      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;

      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 (f </> g) -> continuous;

      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;

      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;

      coherence ;

      cluster (f [#] r) -> continuous;

      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;

      coherence ;

    end

    theorem :: TOPREALC:60

    

     Th60: for r be non negative Real holds for n be non zero Nat, p be 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;

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

      n in NAT by ORDINAL1:def 12;

      then

       A1: the carrier of ( Tcircle (( 0. ( TOP-REAL n)),r)) = ( Sphere (( 0. ( TOP-REAL n)),r)) by TOPREALB: 9;

       |.(( - p1) - ( 0. ( TOP-REAL n))).| = |.( - p1).|

      .= |.p1.| by EUCLID: 71

      .= |.(p1 - ( 0. ( TOP-REAL n))).|

      .= r by A1, TOPREAL9: 9;

      hence thesis by A1, TOPREAL9: 9;

    end;

    theorem :: TOPREALC:61

    

     Th61: for r be non negative Real holds for f be 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;

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

    end;

    definition

      let n be Nat, r be non negative Real;

      let X be Subset of ( Tcircle (( 0. ( TOP-REAL (n + 1))),r));

      :: original: (-)

      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 be object;

          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;

      let X be open Subset of ( Tcircle (( 0. ( TOP-REAL (m + 1))),r));

      cluster ( (-) X) -> open;

      coherence

      proof

        set T = ( Tcircle (( 0. ( TOP-REAL (m + 1))),r));

        ex G be Subset of ( TOP-REAL (m + 1)) st G is open & ( (-) X) = (G /\ the carrier of T)

        proof

          consider G be 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 be object;

            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 be object;

          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 :: TOPREALC:62

    for r be non negative Real holds for f be 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;

      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 be Point of T, r be positive Real holds ex W be 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;

        reconsider q = ( - p) as Point of T by Th60;

        consider W be 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 be Element of T such that

         A3: x in W1 and

         A4: (g . x) = y by FUNCT_2: 65;

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

        hence y in ( Ball ((g . p),r)) by A2, A4, A5;

      end;

      hence thesis by TOPS_4: 18;

    end;