tmap_1.miz



    begin

    registration

      let X be non empty TopSpace;

      let X1,X2 be non empty SubSpace of X;

      cluster (X1 union X2) -> TopSpace-like;

      coherence ;

    end

    definition

      let A,B be non empty set;

      let A1,A2 be non empty Subset of A;

      let f1 be Function of A1, B, f2 be Function of A2, B;

      :: TMAP_1:def1

      func f1 union f2 -> Function of (A1 \/ A2), B equals (f1 +* f2);

      coherence

      proof

        set H = (f1 +* f2);

        ( rng H) c= (( rng f1) \/ ( rng f2)) by FUNCT_4: 17;

        then

         A2: ( rng H) c= B by XBOOLE_1: 1;

        ( dom f1) = A1 & ( dom f2) = A2 by FUNCT_2:def 1;

        then ( dom H) = (A1 \/ A2) by FUNCT_4:def 1;

        hence thesis by A2, FUNCT_2:def 1, RELSET_1: 4;

      end;

    end

    

     Def1: for A,B be non empty set holds for A1,A2 be non empty Subset of A holds for f1 be Function of A1, B, f2 be Function of A2, B st (f1 | (A1 /\ A2)) = (f2 | (A1 /\ A2)) holds ((f1 union f2) | A1) = f1 & ((f1 union f2) | A2) = f2

    proof

      let A,B be non empty set;

      let A1,A2 be non empty Subset of A;

      let f1 be Function of A1, B, f2 be Function of A2, B;

      assume

       A1: (f1 | (A1 /\ A2)) = (f2 | (A1 /\ A2));

      

       A2: ( dom f1) = A1 & ( dom f2) = A2 by FUNCT_2:def 1;

      for x be object st x in (( dom f1) /\ ( dom f2)) holds (f1 . x) = (f2 . x)

      proof

        let x be object;

        assume

         a3: x in (( dom f1) /\ ( dom f2));

        

        then (f1 . x) = ((f1 | (A1 /\ A2)) . x) by A2, FUNCT_1: 49

        .= (f2 . x) by FUNCT_1: 49, a3, A2, A1;

        hence thesis;

      end;

      then (f1 union f2) = (f2 union f1) by FUNCT_4: 34, PARTFUN1:def 4;

      hence thesis by FUNCT_4: 23, A2;

    end;

    theorem :: TMAP_1:1

    

     Th1: for A,B be non empty set, A1,A2 be non empty Subset of A st A1 misses A2 holds for f1 be Function of A1, B, f2 be Function of A2, B holds (f1 | (A1 /\ A2)) = (f2 | (A1 /\ A2)) & ((f1 union f2) | A1) = f1 & ((f1 union f2) | A2) = f2

    proof

      let A,B be non empty set, A1,A2 be non empty Subset of A;

      assume

       A1: A1 misses A2;

      let f1 be Function of A1, B, f2 be Function of A2, B;

      (A1 /\ A2) c= A2 by XBOOLE_1: 17;

      then

      reconsider g2 = (f2 | (A1 /\ A2)) as Function of {} , B by A1, FUNCT_2: 32;

      (A1 /\ A2) c= A1 by XBOOLE_1: 17;

      then

      reconsider g1 = (f1 | (A1 /\ A2)) as Function of {} , B by A1, FUNCT_2: 32;

      g1 = g2;

      hence thesis by Def1;

    end;

    reserve A,B for non empty set,

A1,A2,A3 for non empty Subset of A;

    theorem :: TMAP_1:2

    

     Th2: for g be Function of (A1 \/ A2), B, g1 be Function of A1, B, g2 be Function of A2, B st (g | A1) = g1 & (g | A2) = g2 holds g = (g1 union g2)

    proof

      let g be Function of (A1 \/ A2), B, g1 be Function of A1, B, g2 be Function of A2, B;

      assume

       A1: (g | A1) = g1 & (g | A2) = g2;

      A2 c= (A1 \/ A2) by XBOOLE_1: 7;

      then

      reconsider f2 = (g | A2) as Function of A2, B by FUNCT_2: 32;

      A1 c= (A1 \/ A2) by XBOOLE_1: 7;

      then

      reconsider f1 = (g | A1) as Function of A1, B by FUNCT_2: 32;

      set h = (g1 union g2);

      

       C1: ( dom g) = (A1 \/ A2) by FUNCT_2:def 1

      .= ( dom h) by FUNCT_2:def 1;

      for x be object st x in ( dom g) holds (g . x) = (h . x)

      proof

        let x be object;

        assume x in ( dom g);

        then

         D0: x in A1 or x in A2 by XBOOLE_0:def 3;

        per cases ;

          suppose

           D1: x in ( dom g2);

          

          then (h . x) = (g2 . x) by FUNCT_4: 13

          .= (g . x) by A1, FUNCT_1: 49, D1;

          hence thesis;

        end;

          suppose

           D1: not x in ( dom g2);

          then

           D2: x in A1 by D0, FUNCT_2:def 1;

          (h . x) = (g1 . x) by D1, FUNCT_4: 11

          .= (g . x) by A1, FUNCT_1: 49, D2;

          hence thesis;

        end;

      end;

      hence thesis by C1, FUNCT_1: 2;

    end;

    theorem :: TMAP_1:3

    for f1 be Function of A1, B, f2 be Function of A2, B st (f1 | (A1 /\ A2)) = (f2 | (A1 /\ A2)) holds (f1 union f2) = (f2 union f1)

    proof

      let f1 be Function of A1, B, f2 be Function of A2, B;

      assume (f1 | (A1 /\ A2)) = (f2 | (A1 /\ A2));

      then ((f1 union f2) | A1) = f1 & ((f1 union f2) | A2) = f2 by Def1;

      hence thesis by Th2;

    end;

    theorem :: TMAP_1:4

    for A12,A23 be non empty Subset of A st A12 = (A1 \/ A2) & A23 = (A2 \/ A3) holds for f1 be Function of A1, B, f2 be Function of A2, B, f3 be Function of A3, B st (f1 | (A1 /\ A2)) = (f2 | (A1 /\ A2)) & (f2 | (A2 /\ A3)) = (f3 | (A2 /\ A3)) & (f1 | (A1 /\ A3)) = (f3 | (A1 /\ A3)) holds for f12 be Function of A12, B, f23 be Function of A23, B st f12 = (f1 union f2) & f23 = (f2 union f3) holds (f12 union f3) = (f1 union f23)

    proof

      let A12,A23 be non empty Subset of A such that

       A1: A12 = (A1 \/ A2) and

       A2: A23 = (A2 \/ A3);

      let f1 be Function of A1, B, f2 be Function of A2, B, f3 be Function of A3, B such that

       A3: (f1 | (A1 /\ A2)) = (f2 | (A1 /\ A2)) and

       A4: (f2 | (A2 /\ A3)) = (f3 | (A2 /\ A3)) and

       A5: (f1 | (A1 /\ A3)) = (f3 | (A1 /\ A3));

      let f12 be Function of A12, B, f23 be Function of A23, B such that

       A6: f12 = (f1 union f2) and

       A7: f23 = (f2 union f3);

      

       A8: ((f12 | A2) | (A2 /\ A3)) = (f2 | (A2 /\ A3)) by A3, A6, Def1;

      (A1 \/ A23) = (A12 \/ A3) by A1, A2, XBOOLE_1: 4;

      then

      reconsider f = (f12 union f3) as Function of (A1 \/ A23), B;

      (A12 /\ A3) c= A12 by XBOOLE_1: 17;

      then

      reconsider F = (f12 | (A12 /\ A3)) as Function of (A12 /\ A3), B by FUNCT_2: 32;

      

       A9: (A2 /\ A3) c= A2 by XBOOLE_1: 17;

      

       A10: (f12 | A2) = f2 by A3, A6, Def1;

      A23 c= (A1 \/ A23) by XBOOLE_1: 7;

      then

      reconsider H = (f | A23) as Function of A23, B by FUNCT_2: 32;

      

       A11: A2 c= A12 by A1, XBOOLE_1: 7;

      (A12 /\ A3) c= A3 by XBOOLE_1: 17;

      then

      reconsider G = (f3 | (A12 /\ A3)) as Function of (A12 /\ A3), B by FUNCT_2: 32;

      

       A12: (A1 /\ A3) c= A1 by XBOOLE_1: 17;

      

       A13: ((f12 | A1) | (A1 /\ A3)) = (f1 | (A1 /\ A3)) by A3, A6, Def1;

      now

        let x be object;

        assume

         A14: x in (A12 /\ A3);

        

         A15: (A1 /\ A3) c= (A12 /\ A3) by A1, XBOOLE_1: 7, XBOOLE_1: 26;

         A16:

        now

          assume

           A17: x in (A1 /\ A3);

          

          hence (F . x) = ((F | (A1 /\ A3)) . x) by FUNCT_1: 49

          .= ((f12 | (A1 /\ A3)) . x) by A15, FUNCT_1: 51

          .= ((f3 | (A1 /\ A3)) . x) by A5, A13, A12, FUNCT_1: 51

          .= ((G | (A1 /\ A3)) . x) by A15, FUNCT_1: 51

          .= (G . x) by A17, FUNCT_1: 49;

        end;

        

         A18: (A2 /\ A3) c= (A12 /\ A3) by A1, XBOOLE_1: 7, XBOOLE_1: 26;

         A19:

        now

          assume

           A20: x in (A2 /\ A3);

          

          hence (F . x) = ((F | (A2 /\ A3)) . x) by FUNCT_1: 49

          .= ((f12 | (A2 /\ A3)) . x) by A18, FUNCT_1: 51

          .= ((f3 | (A2 /\ A3)) . x) by A4, A8, A9, FUNCT_1: 51

          .= ((G | (A2 /\ A3)) . x) by A18, FUNCT_1: 51

          .= (G . x) by A20, FUNCT_1: 49;

        end;

        (A12 /\ A3) = ((A1 /\ A3) \/ (A2 /\ A3)) by A1, XBOOLE_1: 23;

        hence (F . x) = (G . x) by A14, A16, A19, XBOOLE_0:def 3;

      end;

      then

       A21: (f12 | (A12 /\ A3)) = (f3 | (A12 /\ A3)) by FUNCT_2: 12;

      then

       A22: ((f | A12) | A1) = (f12 | A1) by Def1;

      ((f | A12) | A2) = (f12 | A2) by A21, Def1;

      then

       A23: (f | A2) = f2 by A10, A11, FUNCT_1: 51;

      now

        let x be object;

        assume

         A24: x in A23;

         A25:

        now

          assume

           A26: x in A2;

          

          thus (H . x) = (f . x) by A24, FUNCT_1: 49

          .= (f2 . x) by A23, A26, FUNCT_1: 49

          .= ((f23 | A2) . x) by A4, A7, Def1

          .= (f23 . x) by A26, FUNCT_1: 49;

        end;

        now

          assume

           A27: x in A3;

          

          thus (H . x) = (f . x) by A24, FUNCT_1: 49

          .= ((f | A3) . x) by A27, FUNCT_1: 49

          .= (f3 . x) by A21, Def1

          .= ((f23 | A3) . x) by A4, A7, Def1

          .= (f23 . x) by A27, FUNCT_1: 49;

        end;

        hence (H . x) = (f23 . x) by A2, A24, A25, XBOOLE_0:def 3;

      end;

      then

       A28: (f | A23) = f23 by FUNCT_2: 12;

      

       A29: A1 c= A12 by A1, XBOOLE_1: 7;

      (f12 | A1) = f1 by A3, A6, Def1;

      then (f | A1) = f1 by A22, A29, FUNCT_1: 51;

      hence thesis by A28, Th2;

    end;

    theorem :: TMAP_1:5

    for f1 be Function of A1, B, f2 be Function of A2, B st (f1 | (A1 /\ A2)) = (f2 | (A1 /\ A2)) holds (A1 is Subset of A2 iff (f1 union f2) = f2) & (A2 is Subset of A1 iff (f1 union f2) = f1)

    proof

      let f1 be Function of A1, B, f2 be Function of A2, B such that

       A1: (f1 | (A1 /\ A2)) = (f2 | (A1 /\ A2));

       A2:

      now

        assume A1 is Subset of A2;

        then A2 = (A1 \/ A2) by XBOOLE_1: 12;

        then ((f1 union f2) | (A1 \/ A2)) = f2 by A1, Def1;

        then ((f1 union f2) * ( id (A1 \/ A2))) = f2 by RELAT_1: 65;

        hence (f1 union f2) = f2 by FUNCT_2: 17;

      end;

      now

        

         A3: ( dom (f1 union f2)) = (A1 \/ A2) & ( dom f2) = A2 by FUNCT_2:def 1;

        assume (f1 union f2) = f2;

        hence A1 is Subset of A2 by A3, XBOOLE_1: 7;

      end;

      hence A1 is Subset of A2 iff (f1 union f2) = f2 by A2;

       A4:

      now

        assume A2 is Subset of A1;

        then A1 = (A1 \/ A2) by XBOOLE_1: 12;

        then ((f1 union f2) | (A1 \/ A2)) = f1 by A1, Def1;

        then ((f1 union f2) * ( id (A1 \/ A2))) = f1 by RELAT_1: 65;

        hence (f1 union f2) = f1 by FUNCT_2: 17;

      end;

      now

        

         A5: ( dom (f1 union f2)) = (A1 \/ A2) & ( dom f1) = A1 by FUNCT_2:def 1;

        assume (f1 union f2) = f1;

        hence A2 is Subset of A1 by A5, XBOOLE_1: 7;

      end;

      hence A2 is Subset of A1 iff (f1 union f2) = f1 by A4;

    end;

    begin

    reserve X for TopSpace;

    theorem :: TMAP_1:6

    

     Th6: for X be TopStruct, X0 be SubSpace of X holds the TopStruct of X0 is strict SubSpace of X

    proof

      let X be TopStruct, X0 be SubSpace of X;

      reconsider S = the TopStruct of X0 as TopStruct;

      S is SubSpace of X

      proof

        

         A1: ( [#] X0) = the carrier of X0;

        hence ( [#] S) c= ( [#] X) by PRE_TOPC:def 4;

        let P be Subset of S;

        thus P in the topology of S implies ex Q be Subset of X st Q in the topology of X & P = (Q /\ ( [#] S)) by A1, PRE_TOPC:def 4;

        given Q be Subset of X such that

         A2: Q in the topology of X & P = (Q /\ ( [#] S));

        thus thesis by A1, A2, PRE_TOPC:def 4;

      end;

      hence thesis;

    end;

    theorem :: TMAP_1:7

    

     Th7: for X be TopStruct holds for X1,X2 be TopSpace st X1 = the TopStruct of X2 holds X1 is SubSpace of X iff X2 is SubSpace of X

    proof

      let X be TopStruct;

      let X1,X2 be TopSpace such that

       A1: X1 = the TopStruct of X2;

      thus X1 is SubSpace of X implies X2 is SubSpace of X

      proof

        

         A2: ( [#] X1) = the carrier of X1;

        assume

         A3: X1 is SubSpace of X;

        hence ( [#] X2) c= ( [#] X) by A1, A2, PRE_TOPC:def 4;

        let P be Subset of X2;

        thus P in the topology of X2 implies ex Q be Subset of X st Q in the topology of X & P = (Q /\ ( [#] X2)) by A1, A3, A2, PRE_TOPC:def 4;

        given Q be Subset of X such that

         A4: Q in the topology of X & P = (Q /\ ( [#] X2));

        thus thesis by A1, A3, A2, A4, PRE_TOPC:def 4;

      end;

      thus thesis by A1, Th6;

    end;

    theorem :: TMAP_1:8

    

     Th8: for X1,X2 be TopSpace st X2 = the TopStruct of X1 holds X1 is closed SubSpace of X iff X2 is closed SubSpace of X

    proof

      let X1,X2 be TopSpace;

      assume

       A1: X2 = the TopStruct of X1;

      thus X1 is closed SubSpace of X implies X2 is closed SubSpace of X

      proof

        assume

         A2: X1 is closed SubSpace of X;

        then

        reconsider Y2 = X2 as SubSpace of X by A1, Th7;

        reconsider A2 = the carrier of Y2 as Subset of X by TSEP_1: 1;

        A2 is closed by A1, A2, TSEP_1: 11;

        hence thesis by TSEP_1: 11;

      end;

      assume

       A3: X2 is closed SubSpace of X;

      then

      reconsider Y1 = X1 as SubSpace of X by A1, Th7;

      reconsider A1 = the carrier of Y1 as Subset of X by TSEP_1: 1;

      A1 is closed by A1, A3, TSEP_1: 11;

      hence thesis by TSEP_1: 11;

    end;

    theorem :: TMAP_1:9

    

     Th9: for X1,X2 be TopSpace st X2 = the TopStruct of X1 holds X1 is open SubSpace of X iff X2 is open SubSpace of X

    proof

      let X1,X2 be TopSpace;

      assume

       A1: X2 = the TopStruct of X1;

      thus X1 is open SubSpace of X implies X2 is open SubSpace of X

      proof

        assume

         A2: X1 is open SubSpace of X;

        then

        reconsider Y2 = X2 as SubSpace of X by A1, Th7;

        reconsider A2 = the carrier of Y2 as Subset of X by TSEP_1: 1;

        A2 is open by A1, A2, TSEP_1: 16;

        hence thesis by TSEP_1: 16;

      end;

      assume

       A3: X2 is open SubSpace of X;

      then

      reconsider Y1 = X1 as SubSpace of X by A1, Th7;

      reconsider A1 = the carrier of Y1 as Subset of X by TSEP_1: 1;

      A1 is open by A1, A3, TSEP_1: 16;

      hence thesis by TSEP_1: 16;

    end;

    reserve X for non empty TopSpace;

    reserve X1,X2 for non empty SubSpace of X;

    theorem :: TMAP_1:10

    

     Th10: X1 is SubSpace of X2 implies for x1 be Point of X1 holds ex x2 be Point of X2 st x2 = x1

    proof

      assume X1 is SubSpace of X2;

      then

       A1: the carrier of X1 c= the carrier of X2 by TSEP_1: 4;

      let x1 be Point of X1;

      x1 in the carrier of X1;

      then

      reconsider x2 = x1 as Point of X2 by A1;

      take x2;

      thus thesis;

    end;

    theorem :: TMAP_1:11

    

     Th11: for x be Point of (X1 union X2) holds (ex x1 be Point of X1 st x1 = x) or ex x2 be Point of X2 st x2 = x

    proof

      let x be Point of (X1 union X2);

      reconsider A0 = the carrier of (X1 union X2) as Subset of X by TSEP_1: 1;

      reconsider A1 = the carrier of X1 as Subset of X by TSEP_1: 1;

      reconsider A2 = the carrier of X2 as Subset of X by TSEP_1: 1;

      assume

       A1: not ex x1 be Point of X1 st x1 = x;

      ex x2 be Point of X2 st x2 = x

      proof

        A0 = (A1 \/ A2) & not x in A1 by A1, TSEP_1:def 2;

        then

        reconsider x2 = x as Point of X2 by XBOOLE_0:def 3;

        take x2;

        thus thesis;

      end;

      hence thesis;

    end;

    theorem :: TMAP_1:12

    

     Th12: X1 meets X2 implies for x be Point of (X1 meet X2) holds (ex x1 be Point of X1 st x1 = x) & ex x2 be Point of X2 st x2 = x

    proof

      assume

       A1: X1 meets X2;

      reconsider A2 = the carrier of X2 as Subset of X by TSEP_1: 1;

      reconsider A1 = the carrier of X1 as Subset of X by TSEP_1: 1;

      reconsider A0 = the carrier of (X1 meet X2) as Subset of X by TSEP_1: 1;

      let x be Point of (X1 meet X2);

      A0 = (A1 /\ A2) by A1, TSEP_1:def 4;

      then x in A1 & x in A2 by XBOOLE_0:def 4;

      hence thesis;

    end;

    theorem :: TMAP_1:13

    for x be Point of (X1 union X2) holds for F1 be Subset of X1, F2 be Subset of X2 st F1 is closed & x in F1 & F2 is closed & x in F2 holds ex H be Subset of (X1 union X2) st H is closed & x in H & H c= (F1 \/ F2)

    proof

      let x be Point of (X1 union X2);

      let F1 be Subset of X1, F2 be Subset of X2 such that

       A1: F1 is closed and

       A2: x in F1 and

       A3: F2 is closed and

       A4: x in F2;

      

       A5: X1 is SubSpace of (X1 union X2) by TSEP_1: 22;

      then

      reconsider C1 = the carrier of X1 as Subset of (X1 union X2) by TSEP_1: 1;

      consider H1 be Subset of (X1 union X2) such that

       A6: H1 is closed and

       A7: (H1 /\ ( [#] X1)) = F1 by A1, A5, PRE_TOPC: 13;

      

       A8: x in H1 by A2, A7, XBOOLE_0:def 4;

      

       A9: X2 is SubSpace of (X1 union X2) by TSEP_1: 22;

      then

      reconsider C2 = the carrier of X2 as Subset of (X1 union X2) by TSEP_1: 1;

      consider H2 be Subset of (X1 union X2) such that

       A10: H2 is closed and

       A11: (H2 /\ ( [#] X2)) = F2 by A3, A9, PRE_TOPC: 13;

      

       A12: x in H2 by A4, A11, XBOOLE_0:def 4;

      take H = (H1 /\ H2);

      

       A13: (H /\ C1) c= (H1 /\ C1) & (H /\ C2) c= (H2 /\ C2) by XBOOLE_1: 17, XBOOLE_1: 26;

      the carrier of (X1 union X2) = (C1 \/ C2) by TSEP_1:def 2;

      

      then H = (H /\ (C1 \/ C2)) by XBOOLE_1: 28

      .= ((H /\ C1) \/ (H /\ C2)) by XBOOLE_1: 23;

      hence thesis by A6, A7, A10, A11, A13, A8, A12, XBOOLE_0:def 4, XBOOLE_1: 13;

    end;

    theorem :: TMAP_1:14

    

     Th14: for x be Point of (X1 union X2) holds for U1 be Subset of X1, U2 be Subset of X2 st U1 is open & x in U1 & U2 is open & x in U2 holds ex V be Subset of (X1 union X2) st V is open & x in V & V c= (U1 \/ U2)

    proof

      let x be Point of (X1 union X2);

      let U1 be Subset of X1, U2 be Subset of X2 such that

       A1: U1 is open and

       A2: x in U1 and

       A3: U2 is open and

       A4: x in U2;

      

       A5: X1 is SubSpace of (X1 union X2) by TSEP_1: 22;

      then

      reconsider C1 = the carrier of X1 as Subset of (X1 union X2) by TSEP_1: 1;

      consider V1 be Subset of (X1 union X2) such that

       A6: V1 is open and

       A7: (V1 /\ ( [#] X1)) = U1 by A1, A5, TOPS_2: 24;

      

       A8: x in V1 by A2, A7, XBOOLE_0:def 4;

      

       A9: X2 is SubSpace of (X1 union X2) by TSEP_1: 22;

      then

      reconsider C2 = the carrier of X2 as Subset of (X1 union X2) by TSEP_1: 1;

      consider V2 be Subset of (X1 union X2) such that

       A10: V2 is open and

       A11: (V2 /\ ( [#] X2)) = U2 by A3, A9, TOPS_2: 24;

      

       A12: x in V2 by A4, A11, XBOOLE_0:def 4;

      take V = (V1 /\ V2);

      

       A13: (V /\ C1) c= (V1 /\ C1) & (V /\ C2) c= (V2 /\ C2) by XBOOLE_1: 17, XBOOLE_1: 26;

      the carrier of (X1 union X2) = (C1 \/ C2) by TSEP_1:def 2;

      

      then V = (V /\ (C1 \/ C2)) by XBOOLE_1: 28

      .= ((V /\ C1) \/ (V /\ C2)) by XBOOLE_1: 23;

      hence thesis by A6, A7, A10, A11, A13, A8, A12, XBOOLE_0:def 4, XBOOLE_1: 13;

    end;

    theorem :: TMAP_1:15

    

     Th15: for x be Point of (X1 union X2) holds for x1 be Point of X1, x2 be Point of X2 st x1 = x & x2 = x holds for A1 be a_neighborhood of x1, A2 be a_neighborhood of x2 holds ex V be Subset of (X1 union X2) st V is open & x in V & V c= (A1 \/ A2)

    proof

      let x be Point of (X1 union X2);

      let x1 be Point of X1, x2 be Point of X2 such that

       A1: x1 = x & x2 = x;

      let A1 be a_neighborhood of x1, A2 be a_neighborhood of x2;

      consider U1 be Subset of X1 such that

       A2: U1 is open and

       A3: U1 c= A1 and

       A4: x1 in U1 by CONNSP_2: 6;

      consider U2 be Subset of X2 such that

       A5: U2 is open and

       A6: U2 c= A2 and

       A7: x2 in U2 by CONNSP_2: 6;

      consider V be Subset of (X1 union X2) such that

       A8: V is open & x in V & V c= (U1 \/ U2) by A1, A2, A4, A5, A7, Th14;

      take V;

      (U1 \/ U2) c= (A1 \/ A2) by A3, A6, XBOOLE_1: 13;

      hence thesis by A8, XBOOLE_1: 1;

    end;

    theorem :: TMAP_1:16

    

     Th16: for x be Point of (X1 union X2) holds for x1 be Point of X1, x2 be Point of X2 st x1 = x & x2 = x holds for A1 be a_neighborhood of x1, A2 be a_neighborhood of x2 holds ex A be a_neighborhood of x st A c= (A1 \/ A2)

    proof

      let x be Point of (X1 union X2);

      let x1 be Point of X1, x2 be Point of X2 such that

       A1: x1 = x & x2 = x;

      let A1 be a_neighborhood of x1, A2 be a_neighborhood of x2;

      consider V be Subset of (X1 union X2) such that

       A2: V is open & x in V and

       A3: V c= (A1 \/ A2) by A1, Th15;

      reconsider W = V as a_neighborhood of x by A2, CONNSP_2: 3;

      take W;

      thus thesis by A3;

    end;

    reserve X0,X1,X2,Y1,Y2 for non empty SubSpace of X;

    theorem :: TMAP_1:17

    

     Th17: X0 is SubSpace of X1 implies X0 meets X1 & X1 meets X0

    proof

      assume X0 is SubSpace of X1;

      then

       A1: the carrier of X0 meets the carrier of X1 by XBOOLE_1: 28, TSEP_1: 4;

      hence X0 meets X1 by TSEP_1:def 3;

      thus thesis by A1, TSEP_1:def 3;

    end;

    theorem :: TMAP_1:18

    

     Th18: X0 is SubSpace of X1 & (X0 meets X2 or X2 meets X0) implies X1 meets X2 & X2 meets X1

    proof

      reconsider A0 = the carrier of X0, A1 = the carrier of X1, A2 = the carrier of X2 as Subset of X by TSEP_1: 1;

      assume X0 is SubSpace of X1;

      then

       A1: A0 c= A1 by TSEP_1: 4;

       A2:

      now

        assume X0 meets X2;

        then A2 meets A0 by TSEP_1:def 3;

        hence thesis by TSEP_1:def 3, A1, XBOOLE_1: 63;

      end;

      assume X0 meets X2 or X2 meets X0;

      hence thesis by A2;

    end;

    theorem :: TMAP_1:19

    

     Th19: X0 is SubSpace of X1 & (X1 misses X2 or X2 misses X1) implies X0 misses X2 & X2 misses X0

    proof

      reconsider A0 = the carrier of X0, A1 = the carrier of X1, A2 = the carrier of X2 as Subset of X by TSEP_1: 1;

      assume X0 is SubSpace of X1;

      then

       A1: A0 c= A1 by TSEP_1: 4;

       A2:

      now

        assume X1 misses X2;

        then A2 misses A1 by TSEP_1:def 3;

        hence thesis by TSEP_1:def 3, A1, XBOOLE_1: 63;

      end;

      assume X1 misses X2 or X2 misses X1;

      hence thesis by A2;

    end;

    theorem :: TMAP_1:20

    (X0 union X0) = the TopStruct of X0

    proof

      X0 is SubSpace of X0 by TSEP_1: 2;

      hence thesis by TSEP_1: 23;

    end;

    theorem :: TMAP_1:21

    (X0 meet X0) = the TopStruct of X0

    proof

      

       A1: X0 is SubSpace of X0 by TSEP_1: 2;

      then X0 meets X0 by Th17;

      hence thesis by A1, TSEP_1: 28;

    end;

    theorem :: TMAP_1:22

    

     Th22: Y1 is SubSpace of X1 & Y2 is SubSpace of X2 implies (Y1 union Y2) is SubSpace of (X1 union X2)

    proof

      assume Y1 is SubSpace of X1 & Y2 is SubSpace of X2;

      then the carrier of Y1 c= the carrier of X1 & the carrier of Y2 c= the carrier of X2 by TSEP_1: 4;

      then (the carrier of Y1 \/ the carrier of Y2) c= (the carrier of X1 \/ the carrier of X2) by XBOOLE_1: 13;

      then the carrier of (Y1 union Y2) c= (the carrier of X1 \/ the carrier of X2) by TSEP_1:def 2;

      then the carrier of (Y1 union Y2) c= the carrier of (X1 union X2) by TSEP_1:def 2;

      hence thesis by TSEP_1: 4;

    end;

    theorem :: TMAP_1:23

    Y1 meets Y2 & Y1 is SubSpace of X1 & Y2 is SubSpace of X2 implies (Y1 meet Y2) is SubSpace of (X1 meet X2)

    proof

      assume

       A1: Y1 meets Y2;

      assume Y1 is SubSpace of X1 & Y2 is SubSpace of X2;

      then

       A2: the carrier of Y1 c= the carrier of X1 & the carrier of Y2 c= the carrier of X2 by TSEP_1: 4;

      the carrier of Y1 meets the carrier of Y2 by A1, TSEP_1:def 3;

      then (the carrier of X1 /\ the carrier of X2) <> {} by A2, XBOOLE_1: 3, XBOOLE_1: 27;

      then the carrier of X1 meets the carrier of X2;

      then

       A3: X1 meets X2 by TSEP_1:def 3;

      (the carrier of Y1 /\ the carrier of Y2) c= (the carrier of X1 /\ the carrier of X2) by A2, XBOOLE_1: 27;

      then (the carrier of Y1 /\ the carrier of Y2) c= the carrier of (X1 meet X2) by A3, TSEP_1:def 4;

      then the carrier of (Y1 meet Y2) c= the carrier of (X1 meet X2) by A1, TSEP_1:def 4;

      hence thesis by TSEP_1: 4;

    end;

    theorem :: TMAP_1:24

    

     Th24: X1 is SubSpace of X0 & X2 is SubSpace of X0 implies (X1 union X2) is SubSpace of X0

    proof

      assume X1 is SubSpace of X0 & X2 is SubSpace of X0;

      then the carrier of X1 c= the carrier of X0 & the carrier of X2 c= the carrier of X0 by TSEP_1: 4;

      then (the carrier of X1 \/ the carrier of X2) c= the carrier of X0 by XBOOLE_1: 8;

      then the carrier of (X1 union X2) c= the carrier of X0 by TSEP_1:def 2;

      hence thesis by TSEP_1: 4;

    end;

    theorem :: TMAP_1:25

    X1 meets X2 & X1 is SubSpace of X0 & X2 is SubSpace of X0 implies (X1 meet X2) is SubSpace of X0

    proof

      assume

       A1: X1 meets X2;

      assume X1 is SubSpace of X0 & X2 is SubSpace of X0;

      then the carrier of X1 c= the carrier of X0 & the carrier of X2 c= the carrier of X0 by TSEP_1: 4;

      then

       A2: (the carrier of X1 \/ the carrier of X2) c= the carrier of X0 by XBOOLE_1: 8;

      (the carrier of X1 /\ the carrier of X2) c= (the carrier of X1 \/ the carrier of X2) by XBOOLE_1: 29;

      then (the carrier of X1 /\ the carrier of X2) c= the carrier of X0 by A2, XBOOLE_1: 1;

      then the carrier of (X1 meet X2) c= the carrier of X0 by A1, TSEP_1:def 4;

      hence thesis by TSEP_1: 4;

    end;

    theorem :: TMAP_1:26

    

     Th26: ((X1 misses X0 or X0 misses X1) & (X2 meets X0 or X0 meets X2) implies ((X1 union X2) meet X0) = (X2 meet X0) & (X0 meet (X1 union X2)) = (X0 meet X2)) & ((X1 meets X0 or X0 meets X1) & (X2 misses X0 or X0 misses X2) implies ((X1 union X2) meet X0) = (X1 meet X0) & (X0 meet (X1 union X2)) = (X0 meet X1))

    proof

      reconsider A0 = the carrier of X0, A1 = the carrier of X1, A2 = the carrier of X2 as Subset of X by TSEP_1: 1;

      thus (X1 misses X0 or X0 misses X1) & (X2 meets X0 or X0 meets X2) implies ((X1 union X2) meet X0) = (X2 meet X0) & (X0 meet (X1 union X2)) = (X0 meet X2)

      proof

        assume that

         A1: X1 misses X0 or X0 misses X1 and

         A2: X2 meets X0 or X0 meets X2;

        

         A3: A1 misses A0 by A1, TSEP_1:def 3;

        X2 is SubSpace of (X1 union X2) by TSEP_1: 22;

        then

         A4: (X1 union X2) meets X0 by A2, Th18;

        

        then

         A5: the carrier of (X0 meet (X1 union X2)) = (A0 /\ the carrier of (X1 union X2)) by TSEP_1:def 4

        .= (A0 /\ (A1 \/ A2)) by TSEP_1:def 2

        .= ((A0 /\ A1) \/ (A0 /\ A2)) by XBOOLE_1: 23

        .= the carrier of (X0 meet X2) by A2, TSEP_1:def 4, A3;

        the carrier of ((X1 union X2) meet X0) = (the carrier of (X1 union X2) /\ A0) by A4, TSEP_1:def 4

        .= ((A1 \/ A2) /\ A0) by TSEP_1:def 2

        .= ((A1 /\ A0) \/ (A2 /\ A0)) by XBOOLE_1: 23

        .= the carrier of (X2 meet X0) by A2, TSEP_1:def 4, A3;

        hence thesis by A5, TSEP_1: 5;

      end;

      thus (X1 meets X0 or X0 meets X1) & (X2 misses X0 or X0 misses X2) implies ((X1 union X2) meet X0) = (X1 meet X0) & (X0 meet (X1 union X2)) = (X0 meet X1)

      proof

        assume that

         A6: X1 meets X0 or X0 meets X1 and

         A7: X2 misses X0 or X0 misses X2;

        

         A8: A2 misses A0 by A7, TSEP_1:def 3;

        X1 is SubSpace of (X1 union X2) by TSEP_1: 22;

        then

         A9: (X1 union X2) meets X0 by A6, Th18;

        

        then

         A10: the carrier of (X0 meet (X1 union X2)) = (A0 /\ the carrier of (X1 union X2)) by TSEP_1:def 4

        .= (A0 /\ (A1 \/ A2)) by TSEP_1:def 2

        .= ((A0 /\ A1) \/ (A0 /\ A2)) by XBOOLE_1: 23

        .= the carrier of (X0 meet X1) by A6, TSEP_1:def 4, A8;

        the carrier of ((X1 union X2) meet X0) = (the carrier of (X1 union X2) /\ A0) by A9, TSEP_1:def 4

        .= ((A1 \/ A2) /\ A0) by TSEP_1:def 2

        .= ((A1 /\ A0) \/ {} ) by A8, XBOOLE_1: 23

        .= the carrier of (X1 meet X0) by A6, TSEP_1:def 4;

        hence thesis by A10, TSEP_1: 5;

      end;

    end;

    theorem :: TMAP_1:27

    

     Th27: X1 meets X2 implies (X1 is SubSpace of X0 implies (X1 meet X2) is SubSpace of (X0 meet X2)) & (X2 is SubSpace of X0 implies (X1 meet X2) is SubSpace of (X1 meet X0))

    proof

      reconsider A0 = the carrier of X0, A1 = the carrier of X1, A2 = the carrier of X2 as Subset of X by TSEP_1: 1;

      assume

       A1: X1 meets X2;

      then

       A2: the carrier of (X1 meet X2) = (A1 /\ A2) by TSEP_1:def 4;

       A3:

      now

        assume

         A4: X2 is SubSpace of X0;

        then

         A5: (A1 /\ A2) c= (A1 /\ A0) by XBOOLE_1: 26, TSEP_1: 4;

        X1 meets X0 by A1, A4, Th18;

        then the carrier of (X1 meet X0) = (A1 /\ A0) by TSEP_1:def 4;

        hence (X1 meet X2) is SubSpace of (X1 meet X0) by A2, A5, TSEP_1: 4;

      end;

      now

        assume

         A6: X1 is SubSpace of X0;

        then A1 c= A0 by TSEP_1: 4;

        then

         A7: (A1 /\ A2) c= (A0 /\ A2) by XBOOLE_1: 26;

        X0 meets X2 by A1, A6, Th18;

        then the carrier of (X0 meet X2) = (A0 /\ A2) by TSEP_1:def 4;

        hence (X1 meet X2) is SubSpace of (X0 meet X2) by A2, A7, TSEP_1: 4;

      end;

      hence thesis by A3;

    end;

    theorem :: TMAP_1:28

    

     Th28: X1 is SubSpace of X0 & (X0 misses X2 or X2 misses X0) implies (X0 meet (X1 union X2)) = the TopStruct of X1 & (X0 meet (X2 union X1)) = the TopStruct of X1

    proof

      reconsider A0 = the carrier of X0, A1 = the carrier of X1, A2 = the carrier of X2 as Subset of X by TSEP_1: 1;

      

       A1: X1 is SubSpace of (X1 union X2) by TSEP_1: 22;

      assume

       A2: X1 is SubSpace of X0;

      then

       A3: A1 c= A0 by TSEP_1: 4;

      assume X0 misses X2 or X2 misses X0;

      then

       A4: A0 misses A2 by TSEP_1:def 3;

      X0 meets X1 by A2, Th17;

      then X0 meets (X1 union X2) by A1, Th18;

      

      then

       A5: the carrier of (X0 meet (X1 union X2)) = (A0 /\ the carrier of (X1 union X2)) by TSEP_1:def 4

      .= (A0 /\ (A1 \/ A2)) by TSEP_1:def 2

      .= ((A0 /\ A1) \/ (A0 /\ A2)) by XBOOLE_1: 23

      .= A1 by A3, XBOOLE_1: 28, A4;

      hence (X0 meet (X1 union X2)) = the TopStruct of X1 by TSEP_1: 5;

      thus thesis by A5, TSEP_1: 5;

    end;

    theorem :: TMAP_1:29

    

     Th29: X1 meets X2 implies (X1 is SubSpace of X0 implies (X0 meet X2) meets X1 & (X2 meet X0) meets X1) & (X2 is SubSpace of X0 implies (X1 meet X0) meets X2 & (X0 meet X1) meets X2)

    proof

      assume

       A1: X1 meets X2;

       A2:

      now

        (X1 meet X2) is SubSpace of X2 by A1, TSEP_1: 27;

        then

         A3: (X1 meet X2) meets X2 by Th17;

        assume

         A4: X2 is SubSpace of X0;

        then (X1 meet X2) is SubSpace of (X1 meet X0) by A1, Th27;

        hence

         A5: (X1 meet X0) meets X2 by A3, Th18;

        X1 meets X0 by A1, A4, Th18;

        hence (X0 meet X1) meets X2 by A5, TSEP_1: 26;

      end;

      now

        (X1 meet X2) is SubSpace of X1 by A1, TSEP_1: 27;

        then

         A6: (X1 meet X2) meets X1 by Th17;

        assume

         A7: X1 is SubSpace of X0;

        then (X1 meet X2) is SubSpace of (X0 meet X2) by A1, Th27;

        hence

         A8: (X0 meet X2) meets X1 by A6, Th18;

        X0 meets X2 by A1, A7, Th18;

        hence (X2 meet X0) meets X1 by A8, TSEP_1: 26;

      end;

      hence thesis by A2;

    end;

    theorem :: TMAP_1:30

    

     Th30: X1 is SubSpace of Y1 & X2 is SubSpace of Y2 & (Y1 misses Y2 or (Y1 meet Y2) misses (X1 union X2)) implies Y1 misses X2 & Y2 misses X1

    proof

      assume that

       A1: X1 is SubSpace of Y1 and

       A2: X2 is SubSpace of Y2;

      assume

       A3: Y1 misses Y2 or (Y1 meet Y2) misses (X1 union X2);

      now

        assume

         A4: not Y1 misses Y2;

         A5:

        now

          assume Y2 meets X1;

          then

           A6: (Y1 meet Y2) meets X1 by A1, Th29;

          X1 is SubSpace of (X1 union X2) by TSEP_1: 22;

          hence contradiction by A3, A4, A6, Th18;

        end;

        now

          assume Y1 meets X2;

          then

           A7: (Y1 meet Y2) meets X2 by A2, Th29;

          X2 is SubSpace of (X1 union X2) by TSEP_1: 22;

          hence contradiction by A3, A4, A7, Th18;

        end;

        hence thesis by A5;

      end;

      hence thesis by A1, A2, Th19;

    end;

    theorem :: TMAP_1:31

    

     Th31: not X1 is SubSpace of X2 & not X2 is SubSpace of X1 & (X1 union X2) is SubSpace of (Y1 union Y2) & (Y1 meet (X1 union X2)) is SubSpace of X1 & (Y2 meet (X1 union X2)) is SubSpace of X2 implies Y1 meets (X1 union X2) & Y2 meets (X1 union X2)

    proof

      assume that

       A1: not X1 is SubSpace of X2 and

       A2: not X2 is SubSpace of X1;

      reconsider A1 = the carrier of X1, A2 = the carrier of X2, C1 = the carrier of Y1, C2 = the carrier of Y2 as Subset of X by TSEP_1: 1;

      assume

       A3: (X1 union X2) is SubSpace of (Y1 union Y2);

      assume that

       A4: (Y1 meet (X1 union X2)) is SubSpace of X1 and

       A5: (Y2 meet (X1 union X2)) is SubSpace of X2;

      

       A6: the carrier of (X1 union X2) = (A1 \/ A2) by TSEP_1:def 2;

      

       A7: the carrier of (Y1 union Y2) = (C1 \/ C2) by TSEP_1:def 2;

       A8:

      now

        assume Y2 misses (X1 union X2);

        then

         A9: C2 misses (A1 \/ A2) by A6, TSEP_1:def 3;

        (A1 \/ A2) c= (C1 \/ C2) by A3, A6, A7, TSEP_1: 4;

        

        then

         A10: (A1 \/ A2) = ((C1 \/ C2) /\ (A1 \/ A2)) by XBOOLE_1: 28

        .= ((C1 /\ (A1 \/ A2)) \/ (C2 /\ (A1 \/ A2))) by XBOOLE_1: 23

        .= (C1 /\ (A1 \/ A2)) by A9;

        then C1 meets (A1 \/ A2);

        then Y1 meets (X1 union X2) by A6, TSEP_1:def 3;

        then the carrier of (Y1 meet (X1 union X2)) = (C1 /\ (A1 \/ A2)) by A6, TSEP_1:def 4;

        then

         A11: (A1 \/ A2) c= A1 by A4, A10, TSEP_1: 4;

        A2 c= (A1 \/ A2) by XBOOLE_1: 7;

        hence contradiction by A2, TSEP_1: 4, A11, XBOOLE_1: 1;

      end;

      now

        assume Y1 misses (X1 union X2);

        then

         A12: C1 misses (A1 \/ A2) by A6, TSEP_1:def 3;

        (A1 \/ A2) c= (C1 \/ C2) by A3, A6, A7, TSEP_1: 4;

        

        then

         A13: (A1 \/ A2) = ((C1 \/ C2) /\ (A1 \/ A2)) by XBOOLE_1: 28

        .= ((C1 /\ (A1 \/ A2)) \/ (C2 /\ (A1 \/ A2))) by XBOOLE_1: 23

        .= (C2 /\ (A1 \/ A2)) by A12;

        then C2 meets (A1 \/ A2);

        then Y2 meets (X1 union X2) by A6, TSEP_1:def 3;

        then the carrier of (Y2 meet (X1 union X2)) = (C2 /\ (A1 \/ A2)) by A6, TSEP_1:def 4;

        then

         A14: (A1 \/ A2) c= A2 by A5, A13, TSEP_1: 4;

        A1 c= (A1 \/ A2) by XBOOLE_1: 7;

        then A1 c= A2 by A14, XBOOLE_1: 1;

        hence contradiction by A1, TSEP_1: 4;

      end;

      hence thesis by A8;

    end;

    theorem :: TMAP_1:32

    

     Th32: X1 meets X2 & not X1 is SubSpace of X2 & not X2 is SubSpace of X1 & the TopStruct of X = ((Y1 union Y2) union X0) & (Y1 meet (X1 union X2)) is SubSpace of X1 & (Y2 meet (X1 union X2)) is SubSpace of X2 & (X0 meet (X1 union X2)) is SubSpace of (X1 meet X2) implies Y1 meets (X1 union X2) & Y2 meets (X1 union X2)

    proof

      assume

       A1: X1 meets X2;

      reconsider C = the carrier of X0 as Subset of X by TSEP_1: 1;

      reconsider C2 = the carrier of Y2 as Subset of X by TSEP_1: 1;

      reconsider C1 = the carrier of Y1 as Subset of X by TSEP_1: 1;

      reconsider A2 = the carrier of X2 as Subset of X by TSEP_1: 1;

      reconsider A1 = the carrier of X1 as Subset of X by TSEP_1: 1;

      assume that

       A2: not X1 is SubSpace of X2 and

       A3: not X2 is SubSpace of X1;

      assume

       A4: the TopStruct of X = ((Y1 union Y2) union X0);

      assume that

       A5: (Y1 meet (X1 union X2)) is SubSpace of X1 and

       A6: (Y2 meet (X1 union X2)) is SubSpace of X2;

      assume

       A7: (X0 meet (X1 union X2)) is SubSpace of (X1 meet X2);

      

       A8: the carrier of (X1 union X2) = (A1 \/ A2) by TSEP_1:def 2;

      

       A9: the carrier of (Y1 union Y2) = (C1 \/ C2) by TSEP_1:def 2;

       A10:

      now

        assume Y2 misses (X1 union X2);

        then

         A11: C2 misses (A1 \/ A2) by A8, TSEP_1:def 3;

        the carrier of X = ((C1 \/ C2) \/ C) by A4, A9, TSEP_1:def 2;

        

        then

         A12: (A1 \/ A2) = (((C2 \/ C1) \/ C) /\ (A1 \/ A2)) by XBOOLE_1: 28

        .= ((C2 \/ (C1 \/ C)) /\ (A1 \/ A2)) by XBOOLE_1: 4

        .= ((C2 /\ (A1 \/ A2)) \/ ((C1 \/ C) /\ (A1 \/ A2))) by XBOOLE_1: 23

        .= ((C1 /\ (A1 \/ A2)) \/ (C /\ (A1 \/ A2))) by XBOOLE_1: 23, A11;

         A13:

        now

          assume (C1 /\ (A1 \/ A2)) <> {} ;

          then C1 meets (A1 \/ A2);

          then Y1 meets (X1 union X2) by A8, TSEP_1:def 3;

          then

           A14: the carrier of (Y1 meet (X1 union X2)) = (C1 /\ (A1 \/ A2)) by A8, TSEP_1:def 4;

          then

           A15: (C1 /\ (A1 \/ A2)) c= A1 by A5, TSEP_1: 4;

          now

            per cases ;

              suppose (C /\ (A1 \/ A2)) = {} ;

              hence (A1 \/ A2) c= A1 by A5, A12, A14, TSEP_1: 4;

            end;

              suppose (C /\ (A1 \/ A2)) <> {} ;

              then C meets (A1 \/ A2);

              then X0 meets (X1 union X2) by A8, TSEP_1:def 3;

              then

               A16: the carrier of (X0 meet (X1 union X2)) = (C /\ (A1 \/ A2)) by A8, TSEP_1:def 4;

              the carrier of (X1 meet X2) = (A1 /\ A2) by A1, TSEP_1:def 4;

              then (C /\ (A1 \/ A2)) c= (A1 /\ A2) by A7, A16, TSEP_1: 4;

              then (A1 \/ A2) c= (A1 \/ (A1 /\ A2)) by A12, A15, XBOOLE_1: 13;

              hence (A1 \/ A2) c= A1 by XBOOLE_1: 12, XBOOLE_1: 17;

            end;

          end;

          hence (A1 \/ A2) c= A1;

        end;

         A17:

        now

          assume (C /\ (A1 \/ A2)) <> {} ;

          then C meets (A1 \/ A2);

          then X0 meets (X1 union X2) by A8, TSEP_1:def 3;

          then

           A18: the carrier of (X0 meet (X1 union X2)) = (C /\ (A1 \/ A2)) by A8, TSEP_1:def 4;

          the carrier of (X1 meet X2) = (A1 /\ A2) by A1, TSEP_1:def 4;

          then

           A19: (C /\ (A1 \/ A2)) c= (A1 /\ A2) by A7, A18, TSEP_1: 4;

          

           A20: (A1 /\ A2) c= A1 by XBOOLE_1: 17;

          then

           A21: (C /\ (A1 \/ A2)) c= A1 by A19, XBOOLE_1: 1;

          now

            per cases ;

              suppose (C1 /\ (A1 \/ A2)) = {} ;

              hence (A1 \/ A2) c= A1 by A12, A19, A20, XBOOLE_1: 1;

            end;

              suppose (C1 /\ (A1 \/ A2)) <> {} ;

              then C1 meets (A1 \/ A2);

              then Y1 meets (X1 union X2) by A8, TSEP_1:def 3;

              then the carrier of (Y1 meet (X1 union X2)) = (C1 /\ (A1 \/ A2)) by A8, TSEP_1:def 4;

              then (C1 /\ (A1 \/ A2)) c= A1 by A5, TSEP_1: 4;

              hence (A1 \/ A2) c= A1 by A12, A21, XBOOLE_1: 8;

            end;

          end;

          hence (A1 \/ A2) c= A1;

        end;

        A2 c= (A1 \/ A2) by XBOOLE_1: 7;

        then A2 c= A1 by A12, A13, A17, XBOOLE_1: 1;

        hence contradiction by A3, TSEP_1: 4;

      end;

      now

        assume Y1 misses (X1 union X2);

        then

         A22: C1 misses (A1 \/ A2) by A8, TSEP_1:def 3;

        the carrier of X = ((C1 \/ C2) \/ C) by A4, A9, TSEP_1:def 2;

        

        then

         A23: (A1 \/ A2) = (((C1 \/ C2) \/ C) /\ (A1 \/ A2)) by XBOOLE_1: 28

        .= ((C1 \/ (C2 \/ C)) /\ (A1 \/ A2)) by XBOOLE_1: 4

        .= ((C1 /\ (A1 \/ A2)) \/ ((C2 \/ C) /\ (A1 \/ A2))) by XBOOLE_1: 23

        .= ((C2 /\ (A1 \/ A2)) \/ (C /\ (A1 \/ A2))) by XBOOLE_1: 23, A22;

         A24:

        now

          assume (C2 /\ (A1 \/ A2)) <> {} ;

          then C2 meets (A1 \/ A2);

          then Y2 meets (X1 union X2) by A8, TSEP_1:def 3;

          then

           A25: the carrier of (Y2 meet (X1 union X2)) = (C2 /\ (A1 \/ A2)) by A8, TSEP_1:def 4;

          then

           A26: (C2 /\ (A1 \/ A2)) c= A2 by A6, TSEP_1: 4;

          now

            per cases ;

              suppose (C /\ (A1 \/ A2)) = {} ;

              hence (A1 \/ A2) c= A2 by A6, A23, A25, TSEP_1: 4;

            end;

              suppose (C /\ (A1 \/ A2)) <> {} ;

              then C meets (A1 \/ A2);

              then X0 meets (X1 union X2) by A8, TSEP_1:def 3;

              then

               A27: the carrier of (X0 meet (X1 union X2)) = (C /\ (A1 \/ A2)) by A8, TSEP_1:def 4;

              the carrier of (X1 meet X2) = (A1 /\ A2) by A1, TSEP_1:def 4;

              then (C /\ (A1 \/ A2)) c= (A1 /\ A2) by A7, A27, TSEP_1: 4;

              then (A1 \/ A2) c= (A2 \/ (A1 /\ A2)) by A23, A26, XBOOLE_1: 13;

              hence (A1 \/ A2) c= A2 by XBOOLE_1: 12, XBOOLE_1: 17;

            end;

          end;

          hence (A1 \/ A2) c= A2;

        end;

         A28:

        now

          assume (C /\ (A1 \/ A2)) <> {} ;

          then C meets (A1 \/ A2);

          then X0 meets (X1 union X2) by A8, TSEP_1:def 3;

          then

           A29: the carrier of (X0 meet (X1 union X2)) = (C /\ (A1 \/ A2)) by A8, TSEP_1:def 4;

          the carrier of (X1 meet X2) = (A1 /\ A2) by A1, TSEP_1:def 4;

          then

           A30: (C /\ (A1 \/ A2)) c= (A1 /\ A2) by A7, A29, TSEP_1: 4;

          

           A31: (A1 /\ A2) c= A2 by XBOOLE_1: 17;

          then

           A32: (C /\ (A1 \/ A2)) c= A2 by A30, XBOOLE_1: 1;

          now

            per cases ;

              suppose (C2 /\ (A1 \/ A2)) = {} ;

              hence (A1 \/ A2) c= A2 by A23, A30, A31, XBOOLE_1: 1;

            end;

              suppose (C2 /\ (A1 \/ A2)) <> {} ;

              then C2 meets (A1 \/ A2);

              then Y2 meets (X1 union X2) by A8, TSEP_1:def 3;

              then the carrier of (Y2 meet (X1 union X2)) = (C2 /\ (A1 \/ A2)) by A8, TSEP_1:def 4;

              then (C2 /\ (A1 \/ A2)) c= A2 by A6, TSEP_1: 4;

              hence (A1 \/ A2) c= A2 by A23, A32, XBOOLE_1: 8;

            end;

          end;

          hence (A1 \/ A2) c= A2;

        end;

        A1 c= (A1 \/ A2) by XBOOLE_1: 7;

        then A1 c= A2 by A23, A24, A28, XBOOLE_1: 1;

        hence contradiction by A2, TSEP_1: 4;

      end;

      hence thesis by A10;

    end;

    theorem :: TMAP_1:33

    

     Th33: X1 meets X2 & not X1 is SubSpace of X2 & not X2 is SubSpace of X1 & not (X1 union X2) is SubSpace of (Y1 union Y2) & the TopStruct of X = ((Y1 union Y2) union X0) & (Y1 meet (X1 union X2)) is SubSpace of X1 & (Y2 meet (X1 union X2)) is SubSpace of X2 & (X0 meet (X1 union X2)) is SubSpace of (X1 meet X2) implies (Y1 union Y2) meets (X1 union X2) & X0 meets (X1 union X2)

    proof

      assume

       A1: X1 meets X2;

      assume

       A2: not X1 is SubSpace of X2 & not X2 is SubSpace of X1;

      reconsider C = the carrier of X0 as Subset of X by TSEP_1: 1;

      reconsider C2 = the carrier of Y2 as Subset of X by TSEP_1: 1;

      reconsider C1 = the carrier of Y1 as Subset of X by TSEP_1: 1;

      reconsider A2 = the carrier of X2 as Subset of X by TSEP_1: 1;

      reconsider A1 = the carrier of X1 as Subset of X by TSEP_1: 1;

      

       A3: the carrier of (Y1 union Y2) = (C1 \/ C2) by TSEP_1:def 2;

      

       A4: Y1 is SubSpace of (Y1 union Y2) by TSEP_1: 22;

      assume

       A5: not (X1 union X2) is SubSpace of (Y1 union Y2);

      assume

       A6: the TopStruct of X = ((Y1 union Y2) union X0);

      assume

       A7: (Y1 meet (X1 union X2)) is SubSpace of X1 & (Y2 meet (X1 union X2)) is SubSpace of X2;

      assume (X0 meet (X1 union X2)) is SubSpace of (X1 meet X2);

      then Y1 meets (X1 union X2) by A1, A2, A6, A7, Th32;

      hence (Y1 union Y2) meets (X1 union X2) by A4, Th18;

      

       A8: the carrier of (X1 union X2) = (A1 \/ A2) by TSEP_1:def 2;

      then

       A9: not (A1 \/ A2) c= (C1 \/ C2) by A5, A3, TSEP_1: 4;

      now

        assume X0 misses (X1 union X2);

        then

         A10: C misses (A1 \/ A2) by A8, TSEP_1:def 3;

        the carrier of X = ((C1 \/ C2) \/ C) by A6, A3, TSEP_1:def 2;

        

        then (A1 \/ A2) = (((C1 \/ C2) \/ C) /\ (A1 \/ A2)) by XBOOLE_1: 28

        .= (((C1 \/ C2) /\ (A1 \/ A2)) \/ (C /\ (A1 \/ A2))) by XBOOLE_1: 23

        .= ((C1 \/ C2) /\ (A1 \/ A2)) by A10;

        hence contradiction by A9, XBOOLE_1: 17;

      end;

      hence thesis;

    end;

    theorem :: TMAP_1:34

    

     Th34: ((X1 union X2) meets X0 iff X1 meets X0 or X2 meets X0) & (X0 meets (X1 union X2) iff X0 meets X1 or X0 meets X2)

    proof

      reconsider A0 = the carrier of X0 as Subset of X by TSEP_1: 1;

      reconsider A1 = the carrier of X1 as Subset of X by TSEP_1: 1;

      reconsider A2 = the carrier of X2 as Subset of X by TSEP_1: 1;

      

       A1: X1 meets X0 or X2 meets X0 implies (X1 union X2) meets X0

      proof

        assume X1 meets X0 or X2 meets X0;

        then A1 meets A0 or A2 meets A0 by TSEP_1:def 3;

        then ((A1 /\ A0) \/ (A2 /\ A0)) <> {} ;

        then ((A1 \/ A2) /\ A0) <> {} by XBOOLE_1: 23;

        then the carrier of (X1 union X2) meets A0 by TSEP_1:def 2;

        hence thesis by TSEP_1:def 3;

      end;

      

       A2: (X1 union X2) meets X0 implies X1 meets X0 or X2 meets X0

      proof

        assume (X1 union X2) meets X0;

        then the carrier of (X1 union X2) meets A0 by TSEP_1:def 3;

        then (the carrier of (X1 union X2) /\ A0) <> {} ;

        then ((A1 \/ A2) /\ A0) <> {} by TSEP_1:def 2;

        then ((A1 /\ A0) \/ (A2 /\ A0)) <> {} by XBOOLE_1: 23;

        then A1 meets A0 or A2 meets A0;

        hence thesis by TSEP_1:def 3;

      end;

      hence (X1 union X2) meets X0 iff X1 meets X0 or X2 meets X0 by A1;

      thus thesis by A2, A1;

    end;

    theorem :: TMAP_1:35

    ((X1 union X2) misses X0 iff X1 misses X0 & X2 misses X0) & (X0 misses (X1 union X2) iff X0 misses X1 & X0 misses X2)

    proof

      reconsider A0 = the carrier of X0 as Subset of X by TSEP_1: 1;

      reconsider A1 = the carrier of X1 as Subset of X by TSEP_1: 1;

      reconsider A2 = the carrier of X2 as Subset of X by TSEP_1: 1;

      

       A1: (X1 union X2) misses X0 implies X1 misses X0 & X2 misses X0

      proof

        assume (X1 union X2) misses X0;

        then the carrier of (X1 union X2) misses A0 by TSEP_1:def 3;

        then ((A1 \/ A2) /\ A0) = {} by TSEP_1:def 2;

        then

         A2: ((A1 /\ A0) \/ (A2 /\ A0)) = {} by XBOOLE_1: 23;

        then

         A3: A2 misses A0;

        (A1 /\ A0) = {} by A2;

        then A1 misses A0;

        hence thesis by A3, TSEP_1:def 3;

      end;

      

       A4: X1 misses X0 & X2 misses X0 implies (X1 union X2) misses X0

      proof

        assume that

         A5: X1 misses X0 and

         A6: X2 misses X0;

        A1 misses A0 by A5, TSEP_1:def 3;

        then

         A7: (A1 /\ A0) = {} ;

        A2 misses A0 by A6, TSEP_1:def 3;

        then ((A1 /\ A0) \/ (A2 /\ A0)) = {} by A7;

        then ((A1 \/ A2) /\ A0) = {} by XBOOLE_1: 23;

        then (the carrier of (X1 union X2) /\ A0) = {} by TSEP_1:def 2;

        then the carrier of (X1 union X2) misses A0;

        hence thesis by TSEP_1:def 3;

      end;

      hence (X1 union X2) misses X0 iff X1 misses X0 & X2 misses X0 by A1;

      thus thesis by A1, A4;

    end;

    theorem :: TMAP_1:36

    X1 meets X2 implies ((X1 meet X2) meets X0 implies X1 meets X0 & X2 meets X0) & (X0 meets (X1 meet X2) implies X0 meets X1 & X0 meets X2)

    proof

      reconsider A0 = the carrier of X0 as Subset of X by TSEP_1: 1;

      reconsider A1 = the carrier of X1 as Subset of X by TSEP_1: 1;

      reconsider A2 = the carrier of X2 as Subset of X by TSEP_1: 1;

      assume

       A1: X1 meets X2;

      thus (X1 meet X2) meets X0 implies X1 meets X0 & X2 meets X0

      proof

        assume (X1 meet X2) meets X0;

        then the carrier of (X1 meet X2) meets A0 by TSEP_1:def 3;

        then ((A1 /\ A2) /\ A0) <> {} by A1, TSEP_1:def 4;

        then

         A2: (A1 /\ (A2 /\ (A0 /\ A0))) <> {} by XBOOLE_1: 16;

        then (A1 /\ (A0 /\ (A2 /\ A0))) <> {} by XBOOLE_1: 16;

        then ((A1 /\ A0) /\ (A2 /\ A0)) <> {} by XBOOLE_1: 16;

        then

         A3: A1 meets A0;

        (A2 /\ A0) <> {} by A2;

        then A2 meets A0;

        hence thesis by A3, TSEP_1:def 3;

      end;

      hence thesis;

    end;

    theorem :: TMAP_1:37

    X1 meets X2 implies (X1 misses X0 or X2 misses X0 implies (X1 meet X2) misses X0) & (X0 misses X1 or X0 misses X2 implies X0 misses (X1 meet X2))

    proof

      reconsider A0 = the carrier of X0 as Subset of X by TSEP_1: 1;

      reconsider A1 = the carrier of X1 as Subset of X by TSEP_1: 1;

      reconsider A2 = the carrier of X2 as Subset of X by TSEP_1: 1;

      assume

       A1: X1 meets X2;

      thus X1 misses X0 or X2 misses X0 implies (X1 meet X2) misses X0

      proof

        assume X1 misses X0 or X2 misses X0;

        then A1 misses A0 or A2 misses A0 by TSEP_1:def 3;

        then ((A1 /\ A0) /\ (A2 /\ A0)) = {} ;

        then (A1 /\ ((A2 /\ A0) /\ A0)) = {} by XBOOLE_1: 16;

        then (A1 /\ (A2 /\ (A0 /\ A0))) = {} by XBOOLE_1: 16;

        then ((A1 /\ A2) /\ A0) = {} by XBOOLE_1: 16;

        then (the carrier of (X1 meet X2) /\ A0) = {} by A1, TSEP_1:def 4;

        then the carrier of (X1 meet X2) misses A0;

        hence thesis by TSEP_1:def 3;

      end;

      hence thesis;

    end;

    theorem :: TMAP_1:38

    

     Th38: for X0 be closed non empty SubSpace of X holds X0 meets X1 implies (X0 meet X1) is closed SubSpace of X1

    proof

      let X0 be closed non empty SubSpace of X;

      reconsider A0 = the carrier of X0 as Subset of X by TSEP_1: 1;

      reconsider A1 = the carrier of X1 as Subset of X by TSEP_1: 1;

      reconsider B = (A0 /\ A1) as Subset of X1 by XBOOLE_1: 17;

      B = (A0 /\ ( [#] X1)) & A0 is closed by TSEP_1: 11;

      then

       A1: B is closed by PRE_TOPC: 13;

      assume

       A2: X0 meets X1;

      then B = the carrier of (X0 meet X1) by TSEP_1:def 4;

      hence thesis by A2, A1, TSEP_1: 11, TSEP_1: 27;

    end;

    theorem :: TMAP_1:39

    

     Th39: for X0 be open non empty SubSpace of X holds X0 meets X1 implies (X0 meet X1) is open SubSpace of X1

    proof

      let X0 be open non empty SubSpace of X;

      reconsider A0 = the carrier of X0 as Subset of X by TSEP_1: 1;

      reconsider A1 = the carrier of X1 as Subset of X by TSEP_1: 1;

      reconsider B = (A0 /\ A1) as Subset of X1 by XBOOLE_1: 17;

      B = (A0 /\ ( [#] X1)) & A0 is open by TSEP_1: 16;

      then

       A1: B is open by TOPS_2: 24;

      assume

       A2: X0 meets X1;

      then B = the carrier of (X0 meet X1) by TSEP_1:def 4;

      hence thesis by A2, A1, TSEP_1: 16, TSEP_1: 27;

    end;

    theorem :: TMAP_1:40

    for X0 be closed non empty SubSpace of X holds X1 is SubSpace of X0 & X0 misses X2 implies X1 is closed SubSpace of (X1 union X2) & X1 is closed SubSpace of (X2 union X1)

    proof

      

       A1: X1 is SubSpace of (X1 union X2) by TSEP_1: 22;

      reconsider S = the TopStruct of X1 as SubSpace of X by Th6;

      let X0 be closed non empty SubSpace of X;

      assume

       A2: X1 is SubSpace of X0;

      assume X0 misses X2;

      then

       A3: (X0 meet (X1 union X2)) = the TopStruct of X1 by A2, Th28;

      X0 meets X1 by A2, Th17;

      then X0 meets (X1 union X2) by A1, Th18;

      then S is closed SubSpace of (X1 union X2) by A3, Th38;

      hence thesis by Th8;

    end;

    theorem :: TMAP_1:41

    

     Th41: for X0 be open non empty SubSpace of X holds X1 is SubSpace of X0 & X0 misses X2 implies X1 is open SubSpace of (X1 union X2) & X1 is open SubSpace of (X2 union X1)

    proof

      

       A1: X1 is SubSpace of (X1 union X2) by TSEP_1: 22;

      reconsider S = the TopStruct of X1 as SubSpace of X by Th6;

      let X0 be open non empty SubSpace of X;

      assume

       A2: X1 is SubSpace of X0;

      assume X0 misses X2;

      then

       A3: (X0 meet (X1 union X2)) = the TopStruct of X1 by A2, Th28;

      X0 meets X1 by A2, Th17;

      then X0 meets (X1 union X2) by A1, Th18;

      then S is open SubSpace of (X1 union X2) by A3, Th39;

      hence thesis by Th9;

    end;

    begin

    definition

      let X,Y be non empty TopSpace, f be Function of X, Y, x be Point of X;

      :: TMAP_1:def2

      pred f is_continuous_at x means for G be a_neighborhood of (f . x) holds ex H be a_neighborhood of x st (f .: H) c= G;

    end

    notation

      let X,Y be non empty TopSpace, f be Function of X, Y, x be Point of X;

      antonym f is_not_continuous_at x for f is_continuous_at x;

    end

    reserve X,Y for non empty TopSpace;

    reserve f for Function of X, Y;

    theorem :: TMAP_1:42

    

     Th42: for x be Point of X holds f is_continuous_at x iff for G be a_neighborhood of (f . x) holds (f " G) is a_neighborhood of x

    proof

      let x be Point of X;

      thus f is_continuous_at x implies for G be a_neighborhood of (f . x) holds (f " G) is a_neighborhood of x

      proof

        assume

         A1: f is_continuous_at x;

        let G be a_neighborhood of (f . x);

        consider H be a_neighborhood of x such that

         A2: (f .: H) c= G by A1;

        ex V be Subset of X st V is open & V c= (f " G) & x in V

        proof

          consider V be Subset of X such that

           A3: V is open & V c= H & x in V by CONNSP_2: 6;

          take V;

          H c= (f " G) by A2, FUNCT_2: 95;

          hence thesis by A3, XBOOLE_1: 1;

        end;

        hence thesis by CONNSP_2: 6;

      end;

      assume

       A4: for G be a_neighborhood of (f . x) holds (f " G) is a_neighborhood of x;

      let G be a_neighborhood of (f . x);

      reconsider H = (f " G) as a_neighborhood of x by A4;

      take H;

      thus thesis by FUNCT_1: 75;

    end;

    theorem :: TMAP_1:43

    

     Th43: for x be Point of X holds f is_continuous_at x iff for G be Subset of Y st G is open & (f . x) in G holds ex H be Subset of X st H is open & x in H & (f .: H) c= G

    proof

      let x be Point of X;

      thus f is_continuous_at x implies for G be Subset of Y st G is open & (f . x) in G holds ex H be Subset of X st H is open & x in H & (f .: H) c= G

      proof

        assume

         A1: f is_continuous_at x;

        let G be Subset of Y;

        assume G is open & (f . x) in G;

        then

        reconsider G0 = G as a_neighborhood of (f . x) by CONNSP_2: 3;

        consider H0 be a_neighborhood of x such that

         A2: (f .: H0) c= G0 by A1;

        consider H be Subset of X such that

         A3: H is open and

         A4: H c= H0 and

         A5: x in H by CONNSP_2: 6;

        take H;

        (f .: H) c= (f .: H0) by A4, RELAT_1: 123;

        hence thesis by A2, A3, A5, XBOOLE_1: 1;

      end;

      assume

       A6: for G be Subset of Y st G is open & (f . x) in G holds ex H be Subset of X st H is open & x in H & (f .: H) c= G;

      let G0 be a_neighborhood of (f . x);

      consider G be Subset of Y such that

       A7: G is open and

       A8: G c= G0 and

       A9: (f . x) in G by CONNSP_2: 6;

      consider H be Subset of X such that

       A10: H is open & x in H and

       A11: (f .: H) c= G by A6, A7, A9;

      reconsider H0 = H as a_neighborhood of x by A10, CONNSP_2: 3;

      take H0;

      thus thesis by A8, A11, XBOOLE_1: 1;

    end;

    theorem :: TMAP_1:44

    

     Th44: f is continuous iff for x be Point of X holds f is_continuous_at x

    proof

      thus f is continuous implies for x be Point of X holds f is_continuous_at x;

      assume

       A1: for x be Point of X holds f is_continuous_at x;

      thus f is continuous

      proof

        let x be Point of X, G be a_neighborhood of (f . x);

        f is_continuous_at x by A1;

        hence thesis;

      end;

    end;

    theorem :: TMAP_1:45

    

     Th45: for X,Y,Z be non empty TopSpace st the carrier of Y = the carrier of Z & the topology of Z c= the topology of Y holds for f be Function of X, Y, g be Function of X, Z st f = g holds for x be Point of X holds f is_continuous_at x implies g is_continuous_at x

    proof

      let X,Y,Z be non empty TopSpace;

      assume that

       A1: the carrier of Y = the carrier of Z and

       A2: the topology of Z c= the topology of Y;

      let f be Function of X, Y, g be Function of X, Z;

      assume

       A3: f = g;

      let x be Point of X;

      assume

       A4: f is_continuous_at x;

      for G be Subset of Z st G is open & (g . x) in G holds ex H be Subset of X st H is open & x in H & (g .: H) c= G

      proof

        let G be Subset of Z;

        reconsider F = G as Subset of Y by A1;

        assume that

         A5: G is open and

         A6: (g . x) in G;

        G in the topology of Z by A5;

        then F is open by A2;

        then

        consider H be Subset of X such that

         A7: H is open & x in H & (f .: H) c= F by A3, A4, A6, Th43;

        take H;

        thus thesis by A3, A7;

      end;

      hence thesis by Th43;

    end;

    theorem :: TMAP_1:46

    

     Th46: for X,Y,Z be non empty TopSpace st the carrier of X = the carrier of Y & the topology of Y c= the topology of X holds for f be Function of X, Z, g be Function of Y, Z st f = g holds for x be Point of X, y be Point of Y st x = y holds g is_continuous_at y implies f is_continuous_at x

    proof

      let X,Y,Z be non empty TopSpace;

      assume that

       A1: the carrier of X = the carrier of Y and

       A2: the topology of Y c= the topology of X;

      let f be Function of X, Z, g be Function of Y, Z;

      assume

       A3: f = g;

      let x be Point of X, y be Point of Y;

      assume

       A4: x = y;

      assume

       A5: g is_continuous_at y;

      for G be Subset of Z st G is open & (f . x) in G holds ex H be Subset of X st H is open & x in H & (f .: H) c= G

      proof

        let G be Subset of Z;

        assume G is open & (f . x) in G;

        then

        consider H be Subset of Y such that

         A6: H is open and

         A7: y in H & (g .: H) c= G by A3, A4, A5, Th43;

        reconsider F = H as Subset of X by A1;

        take F;

        H in the topology of Y by A6;

        hence thesis by A2, A3, A4, A7;

      end;

      hence thesis by Th43;

    end;

    reserve X,Y,Z for non empty TopSpace;

    reserve f for Function of X, Y,

g for Function of Y, Z;

    theorem :: TMAP_1:47

    

     Th47: for x be Point of X, y be Point of Y st y = (f . x) holds f is_continuous_at x & g is_continuous_at y implies (g * f) is_continuous_at x

    proof

      let x be Point of X, y be Point of Y such that

       A1: y = (f . x);

      assume that

       A2: f is_continuous_at x and

       A3: g is_continuous_at y;

      for G be a_neighborhood of ((g * f) . x) holds ((g * f) " G) is a_neighborhood of x

      proof

        let G be a_neighborhood of ((g * f) . x);

        ((g * f) . x) = (g . y) by A1, FUNCT_2: 15;

        then (g " G) is a_neighborhood of (f . x) by A1, A3, Th42;

        then (f " (g " G)) is a_neighborhood of x by A2, Th42;

        hence thesis by RELAT_1: 146;

      end;

      hence thesis by Th42;

    end;

    theorem :: TMAP_1:48

    for y be Point of Y holds f is continuous & g is_continuous_at y implies for x be Point of X st x in (f " {y}) holds (g * f) is_continuous_at x

    proof

      let y be Point of Y;

      assume

       A1: f is continuous;

      assume

       A2: g is_continuous_at y;

      let x be Point of X;

      assume x in (f " {y});

      then {x} is Subset of (f " {y}) by SUBSET_1: 41;

      then ( dom f) = ( [#] X) & ( Im (f,x)) c= {y} by FUNCT_2: 95, FUNCT_2:def 1;

      then

       A3: {(f . x)} c= {y} by FUNCT_1: 59;

      (f . x) in {(f . x)} by TARSKI:def 1;

      then

       A4: (f . x) = y by A3, TARSKI:def 1;

      f is_continuous_at x by A1;

      hence thesis by A2, A4, Th47;

    end;

    theorem :: TMAP_1:49

    for x be Point of X holds f is_continuous_at x & g is continuous implies (g * f) is_continuous_at x

    proof

      let x be Point of X;

      assume

       A1: f is_continuous_at x;

      assume g is continuous;

      then g is_continuous_at (f . x);

      hence thesis by A1, Th47;

    end;

    theorem :: TMAP_1:50

    f is continuous Function of X, Y iff for x be Point of X holds f is_continuous_at x by Th44;

    theorem :: TMAP_1:51

    

     Th51: for X,Y,Z be non empty TopSpace st the carrier of Y = the carrier of Z & the topology of Z c= the topology of Y holds for f be continuous Function of X, Y holds f is continuous Function of X, Z

    proof

      let X,Y,Z be non empty TopSpace;

      assume that

       A1: the carrier of Y = the carrier of Z and

       A2: the topology of Z c= the topology of Y;

      let f be continuous Function of X, Y;

      reconsider g = f as Function of X, Z by A1;

      for x be Point of X holds g is_continuous_at x by Th44, A1, A2, Th45;

      hence thesis by Th44;

    end;

    theorem :: TMAP_1:52

    for X,Y,Z be non empty TopSpace st the carrier of X = the carrier of Y & the topology of Y c= the topology of X holds for f be continuous Function of Y, Z holds f is continuous Function of X, Z

    proof

      let X,Y,Z be non empty TopSpace;

      assume that

       A1: the carrier of X = the carrier of Y and

       A2: the topology of Y c= the topology of X;

      let f be continuous Function of Y, Z;

      reconsider g = f as Function of X, Z by A1;

      for x be Point of X holds g is_continuous_at x by A1, Th44, A2, Th46;

      hence thesis by Th44;

    end;

    

     Lm1: for A be set holds {} is Function of A, {}

    proof

      let A be set;

      per cases ;

        suppose

         A1: A = {} ;

        reconsider f = {} as PartFunc of A, {} by RELSET_1: 12;

        f is total by A1;

        hence thesis;

      end;

        suppose A <> {} ;

        thus thesis by FUNCT_2:def 1, RELSET_1: 12;

      end;

    end;

    definition

      let S,T be 1-sorted;

      let f be Function of S, T;

      let R be 1-sorted;

      :: TMAP_1:def3

      func f | R -> Function of R, T equals

      : Def3: (f | the carrier of R);

      coherence

      proof

        per cases ;

          suppose the carrier of T = {} implies the carrier of S = {} ;

          hence thesis by A1, FUNCT_2: 32;

        end;

          suppose

           A2: the carrier of T = {} & the carrier of S <> {} ;

          then (f | the carrier of R) = {} ;

          hence thesis by A2, Lm1;

        end;

      end;

    end

    definition

      let X,Y be non empty TopSpace, f be Function of X, Y;

      let X0 be SubSpace of X;

      :: original: |

      redefine

      :: TMAP_1:def4

      func f | X0 equals (f | the carrier of X0);

      compatibility

      proof

        ( [#] X0) c= ( [#] X) by PRE_TOPC:def 4;

        hence thesis by Def3;

      end;

    end

    reserve X,Y for non empty TopSpace,

X0 for non empty SubSpace of X;

    reserve f for Function of X, Y;

    theorem :: TMAP_1:53

    

     Th53: for f0 be Function of X0, Y st for x be Point of X st x in the carrier of X0 holds (f . x) = (f0 . x) holds (f | X0) = f0

    proof

      let f0 be Function of X0, Y;

      the carrier of X0 is Subset of X by TSEP_1: 1;

      hence thesis by FUNCT_2: 96;

    end;

    theorem :: TMAP_1:54

    

     Th54: the TopStruct of X0 = the TopStruct of X implies f = (f | X0)

    proof

      assume the TopStruct of X0 = the TopStruct of X;

      

      hence (f | X0) = (f * ( id the carrier of X)) by RELAT_1: 65

      .= f by FUNCT_2: 17;

    end;

    theorem :: TMAP_1:55

    for A be Subset of X st A c= the carrier of X0 holds (f .: A) = ((f | X0) .: A) by FUNCT_2: 97;

    theorem :: TMAP_1:56

    for B be Subset of Y st (f " B) c= the carrier of X0 holds (f " B) = ((f | X0) " B) by FUNCT_2: 98;

    theorem :: TMAP_1:57

    

     Th57: for g be Function of X0, Y holds ex h be Function of X, Y st (h | X0) = g

    proof

      let g be Function of X0, Y;

      now

        per cases ;

          suppose

           A1: the TopStruct of X = the TopStruct of X0;

          then

          reconsider h = g as Function of X, Y;

          take h;

          thus (h | X0) = g by A1, Th54;

        end;

          suppose

           A2: the TopStruct of X <> the TopStruct of X0;

          Y is SubSpace of Y by TSEP_1: 2;

          then

          reconsider B = the carrier of Y as non empty Subset of Y by TSEP_1: 1;

          set y = the Element of B;

          reconsider A0 = the carrier of X0 as Subset of X by TSEP_1: 1;

          

           A3: X is SubSpace of X by TSEP_1: 2;

          then

          reconsider A = the carrier of X as non empty Subset of X by TSEP_1: 1;

          reconsider A1 = (A \ A0) as Subset of X;

          

           A4: A0 misses A1 by XBOOLE_1: 79;

          A0 <> A by A2, A3, TSEP_1: 5;

          then

          reconsider A1 as non empty Subset of A by XBOOLE_1: 37;

          reconsider g1 = (A1 --> y) as Function of A1, B;

          reconsider A0 as non empty Subset of A;

          reconsider g0 = g as Function of A0, B;

          set G = (g0 union g1);

          the carrier of X = (A1 \/ A0) by XBOOLE_1: 45;

          then

          reconsider h = G as Function of X, Y;

          take h;

          thus (h | X0) = g by A4, Th1;

        end;

      end;

      hence thesis;

    end;

    reserve f for Function of X, Y,

X0 for non empty SubSpace of X;

    theorem :: TMAP_1:58

    

     Th58: for x be Point of X, x0 be Point of X0 st x = x0 holds f is_continuous_at x implies (f | X0) is_continuous_at x0

    proof

      let x be Point of X, x0 be Point of X0 such that

       A1: x = x0;

      assume

       A2: f is_continuous_at x;

      for G be Subset of Y st G is open & ((f | X0) . x0) in G holds ex H0 be Subset of X0 st H0 is open & x0 in H0 & ((f | X0) .: H0) c= G

      proof

        reconsider C = the carrier of X0 as Subset of X by TSEP_1: 1;

        let G be Subset of Y such that

         A3: G is open and

         A4: ((f | X0) . x0) in G;

        (f . x) in G by A1, A4, FUNCT_1: 49;

        then

        consider H be Subset of X such that

         A5: H is open & x in H and

         A6: (f .: H) c= G by A2, A3, Th43;

        reconsider H0 = (H /\ C) as Subset of X0 by XBOOLE_1: 17;

        (f .: H0) c= ((f .: H) /\ (f .: C)) & ((f .: H) /\ (f .: C)) c= (f .: H) by RELAT_1: 121, XBOOLE_1: 17;

        then (f .: H0) c= (f .: H) by XBOOLE_1: 1;

        then

         A7: (f .: H0) c= G by A6, XBOOLE_1: 1;

        take H0;

        H0 = (H /\ ( [#] X0)) & ((f | X0) .: H0) c= (f .: H0) by RELAT_1: 128;

        hence thesis by A1, A5, A7, TOPS_2: 24, XBOOLE_0:def 4, XBOOLE_1: 1;

      end;

      hence thesis by Th43;

    end;

    theorem :: TMAP_1:59

    

     Th59: for A be Subset of X, x be Point of X, x0 be Point of X0 st A c= the carrier of X0 & A is a_neighborhood of x & x = x0 holds f is_continuous_at x iff (f | X0) is_continuous_at x0

    proof

      let A be Subset of X, x be Point of X, x0 be Point of X0 such that

       A1: A c= the carrier of X0 and

       A2: A is a_neighborhood of x and

       A3: x = x0;

      thus f is_continuous_at x implies (f | X0) is_continuous_at x0 by A3, Th58;

      thus (f | X0) is_continuous_at x0 implies f is_continuous_at x

      proof

        assume

         A4: (f | X0) is_continuous_at x0;

        for G be Subset of Y st G is open & (f . x) in G holds ex H be Subset of X st H is open & x in H & (f .: H) c= G

        proof

          let G be Subset of Y such that

           A5: G is open and

           A6: (f . x) in G;

          ((f | X0) . x0) in G by A3, A6, FUNCT_1: 49;

          then

          consider H0 be Subset of X0 such that

           A7: H0 is open and

           A8: x0 in H0 and

           A9: ((f | X0) .: H0) c= G by A4, A5, Th43;

          consider V be Subset of X such that

           A10: V is open and

           A11: V c= A and

           A12: x in V by A2, CONNSP_2: 6;

          reconsider V0 = V as Subset of X0 by A1, A11, XBOOLE_1: 1;

          

           A13: (H0 /\ V0) c= V by XBOOLE_1: 17;

          then

          reconsider H = (H0 /\ V0) as Subset of X by XBOOLE_1: 1;

          

           A14: for z be Point of Y holds z in (f .: H) implies z in G

          proof

            set g = (f | X0);

            let z be Point of Y;

            assume z in (f .: H);

            then

            consider y be Point of X such that

             A15: y in H and

             A16: z = (f . y) by FUNCT_2: 65;

            y in V by A13, A15;

            then y in A by A11;

            then

             A17: z = (g . y) by A1, A16, FUNCT_1: 49;

            (H0 /\ V0) c= H0 by XBOOLE_1: 17;

            then z in (g .: H0) by A15, A17, FUNCT_2: 35;

            hence thesis by A9;

          end;

          take H;

          V0 is open by A10, TOPS_2: 25;

          then (H0 /\ V0) is open by A7;

          hence thesis by A3, A8, A10, A12, A13, A14, SUBSET_1: 2, TSEP_1: 9, XBOOLE_0:def 4;

        end;

        hence thesis by Th43;

      end;

    end;

    theorem :: TMAP_1:60

    

     Th60: for A be Subset of X, x be Point of X, x0 be Point of X0 st A is open & x in A & A c= the carrier of X0 & x = x0 holds f is_continuous_at x iff (f | X0) is_continuous_at x0

    proof

      let A be Subset of X, x be Point of X, x0 be Point of X0 such that

       A1: A is open & x in A and

       A2: A c= the carrier of X0 and

       A3: x = x0;

      thus f is_continuous_at x implies (f | X0) is_continuous_at x0 by A3, Th58;

      thus (f | X0) is_continuous_at x0 implies f is_continuous_at x

      proof

        assume

         A4: (f | X0) is_continuous_at x0;

        A is a_neighborhood of x by A1, CONNSP_2: 3;

        hence thesis by A2, A3, A4, Th59;

      end;

    end;

    theorem :: TMAP_1:61

    for X0 be open non empty SubSpace of X, x be Point of X, x0 be Point of X0 st x = x0 holds f is_continuous_at x iff (f | X0) is_continuous_at x0

    proof

      let X0 be open non empty SubSpace of X, x be Point of X, x0 be Point of X0;

      assume

       A1: x = x0;

      hence f is_continuous_at x implies (f | X0) is_continuous_at x0 by Th58;

      thus (f | X0) is_continuous_at x0 implies f is_continuous_at x

      proof

        reconsider A = the carrier of X0 as Subset of X by TSEP_1: 1;

        assume

         A2: (f | X0) is_continuous_at x0;

        A is open by TSEP_1: 16;

        hence thesis by A1, A2, Th60;

      end;

    end;

    registration

      let X, Y;

      let f be continuous Function of X, Y, X0 be non empty SubSpace of X;

      cluster (f | X0) -> continuous;

      coherence

      proof

        for x0 be Point of X0 holds (f | X0) is_continuous_at x0

        proof

          let x0 be Point of X0;

          the carrier of X0 c= the carrier of X & x0 in the carrier of X0 by BORSUK_1: 1;

          then

          reconsider x = x0 as Point of X;

          f is_continuous_at x by Th44;

          hence thesis by Th58;

        end;

        hence thesis by Th44;

      end;

    end

    theorem :: TMAP_1:62

    

     Th62: for X,Y,Z be non empty TopSpace, X0 be non empty SubSpace of X, f be Function of X, Y, g be Function of Y, Z holds ((g * f) | X0) = (g * (f | X0))

    proof

      let X,Y,Z be non empty TopSpace, X0 be non empty SubSpace of X, f be Function of X, Y, g be Function of Y, Z;

      set h = (g * f);

      (h | X0) = (h | the carrier of X0);

      then

      reconsider G = (h | the carrier of X0) as Function of X0, Z;

      (f | X0) = (f | the carrier of X0);

      then

      reconsider F0 = (f | the carrier of X0) as Function of X0, Y;

      set F = (g * F0);

      for x be Point of X0 holds (G . x) = (F . x)

      proof

        let x be Point of X0;

        the carrier of X0 c= the carrier of X by BORSUK_1: 1;

        then

        reconsider y = x as Element of X by TARSKI:def 3;

        

        thus (G . x) = ((g * f) . y) by FUNCT_1: 49

        .= (g . (f . y)) by FUNCT_2: 15

        .= (g . (F0 . x)) by FUNCT_1: 49

        .= (F . x) by FUNCT_2: 15;

      end;

      hence thesis by FUNCT_2: 63;

    end;

    theorem :: TMAP_1:63

    

     Th63: for X,Y,Z be non empty TopSpace, X0 be non empty SubSpace of X, g be Function of Y, Z, f be Function of X, Y st g is continuous & (f | X0) is continuous holds ((g * f) | X0) is continuous

    proof

      let X,Y,Z be non empty TopSpace, X0 be non empty SubSpace of X, g be Function of Y, Z, f be Function of X, Y such that

       A1: g is continuous & (f | X0) is continuous;

      ((g * f) | X0) = (g * (f | X0)) by Th62;

      hence thesis by A1;

    end;

    theorem :: TMAP_1:64

    for X,Y,Z be non empty TopSpace, X0 be non empty SubSpace of X, g be continuous Function of Y, Z, f be Function of X, Y st (f | X0) is continuous Function of X0, Y holds ((g * f) | X0) is continuous Function of X0, Z by Th63;

    definition

      let X,Y be non empty TopSpace, X0,X1 be SubSpace of X, g be Function of X0, Y;

      assume

       A1: X1 is SubSpace of X0;

      :: TMAP_1:def5

      func g | X1 -> Function of X1, Y equals

      : Def5: (g | the carrier of X1);

      coherence

      proof

        the carrier of X1 c= the carrier of X0 by A1, TSEP_1: 4;

        hence thesis by FUNCT_2: 32;

      end;

    end

    reserve X,Y for non empty TopSpace,

X0,X1 for non empty SubSpace of X;

    reserve f for Function of X, Y,

g for Function of X0, Y;

    theorem :: TMAP_1:65

    

     Th65: X1 is SubSpace of X0 implies for x0 be Point of X0 st x0 in the carrier of X1 holds (g . x0) = ((g | X1) . x0)

    proof

      assume

       A1: X1 is SubSpace of X0;

      let x0 be Point of X0;

      assume x0 in the carrier of X1;

      

      hence (g . x0) = ((g | the carrier of X1) . x0) by FUNCT_1: 49

      .= ((g | X1) . x0) by A1, Def5;

    end;

    theorem :: TMAP_1:66

    X1 is SubSpace of X0 implies for g1 be Function of X1, Y st for x0 be Point of X0 st x0 in the carrier of X1 holds (g . x0) = (g1 . x0) holds (g | X1) = g1

    proof

      assume

       A1: X1 is SubSpace of X0;

      then

       A2: the carrier of X1 is Subset of X0 by TSEP_1: 1;

      let g1 be Function of X1, Y;

      assume for x0 be Point of X0 st x0 in the carrier of X1 holds (g . x0) = (g1 . x0);

      then (g | the carrier of X1) = g1 by A2, FUNCT_2: 96;

      hence thesis by A1, Def5;

    end;

    theorem :: TMAP_1:67

    

     Th67: g = (g | X0)

    proof

      X0 is SubSpace of X0 by TSEP_1: 2;

      

      hence (g | X0) = (g | the carrier of X0) by Def5

      .= (g * ( id the carrier of X0)) by RELAT_1: 65

      .= g by FUNCT_2: 17;

    end;

    theorem :: TMAP_1:68

    

     Th68: X1 is SubSpace of X0 implies for A be Subset of X0 st A c= the carrier of X1 holds (g .: A) = ((g | X1) .: A)

    proof

      assume

       A1: X1 is SubSpace of X0;

      let A be Subset of X0;

      assume A c= the carrier of X1;

      

      hence (g .: A) = ((g | the carrier of X1) .: A) by FUNCT_2: 97

      .= ((g | X1) .: A) by A1, Def5;

    end;

    theorem :: TMAP_1:69

    X1 is SubSpace of X0 implies for B be Subset of Y st (g " B) c= the carrier of X1 holds (g " B) = ((g | X1) " B)

    proof

      assume

       A1: X1 is SubSpace of X0;

      let B be Subset of Y;

      assume (g " B) c= the carrier of X1;

      

      hence (g " B) = ((g | the carrier of X1) " B) by FUNCT_2: 98

      .= ((g | X1) " B) by A1, Def5;

    end;

    theorem :: TMAP_1:70

    

     Th70: for g be Function of X0, Y st g = (f | X0) holds X1 is SubSpace of X0 implies (g | X1) = (f | X1)

    proof

      let g be Function of X0, Y;

      assume

       A1: g = (f | X0);

      assume

       A2: X1 is SubSpace of X0;

      then

       A3: the carrier of X1 c= the carrier of X0 by TSEP_1: 4;

      

      thus (g | X1) = (g | the carrier of X1) by A2, Def5

      .= (f | X1) by A1, A3, FUNCT_1: 51;

    end;

    theorem :: TMAP_1:71

    

     Th71: X1 is SubSpace of X0 implies ((f | X0) | X1) = (f | X1)

    proof

      assume

       A1: X1 is SubSpace of X0;

      then

       A2: the carrier of X1 c= the carrier of X0 by TSEP_1: 4;

      (f | X0) = (f | the carrier of X0);

      then

      reconsider h = (f | the carrier of X0) as Function of X0, Y;

      

      thus ((f | X0) | X1) = (h | the carrier of X1) by A1, Def5

      .= (f | X1) by A2, FUNCT_1: 51;

    end;

    theorem :: TMAP_1:72

    

     Th72: for X0,X1,X2 be non empty SubSpace of X st X1 is SubSpace of X0 & X2 is SubSpace of X1 holds for g be Function of X0, Y holds ((g | X1) | X2) = (g | X2)

    proof

      let X0,X1,X2 be non empty SubSpace of X such that

       A1: X1 is SubSpace of X0 and

       A2: X2 is SubSpace of X1;

      

       A3: X2 is SubSpace of X0 by A1, A2, TSEP_1: 7;

      let g be Function of X0, Y;

      set h = (g | X1);

      

       A4: h = (g | the carrier of X1) & the carrier of X2 c= the carrier of X1 by A1, A2, Def5, TSEP_1: 4;

      

      thus (h | X2) = (h | the carrier of X2) by A2, Def5

      .= (g | the carrier of X2) by A4, FUNCT_1: 51

      .= (g | X2) by A3, Def5;

    end;

    theorem :: TMAP_1:73

    for f be Function of X, Y, f0 be Function of X1, Y, g be Function of X0, Y holds X0 = X & f = g implies ((g | X1) = f0 iff (f | X1) = f0) by Def5;

    reserve X0,X1,X2 for non empty SubSpace of X;

    reserve f for Function of X, Y,

g for Function of X0, Y;

    theorem :: TMAP_1:74

    

     Th74: for x0 be Point of X0, x1 be Point of X1 st x0 = x1 holds X1 is SubSpace of X0 & g is_continuous_at x0 implies (g | X1) is_continuous_at x1

    proof

      let x0 be Point of X0, x1 be Point of X1 such that

       A1: x0 = x1;

      assume

       A2: X1 is SubSpace of X0;

      assume

       A3: g is_continuous_at x0;

      for G be Subset of Y st G is open & ((g | X1) . x1) in G holds ex H0 be Subset of X1 st H0 is open & x1 in H0 & ((g | X1) .: H0) c= G

      proof

        reconsider C = the carrier of X1 as Subset of X0 by A2, TSEP_1: 1;

        let G be Subset of Y such that

         A4: G is open and

         A5: ((g | X1) . x1) in G;

        (g . x0) in G by A1, A2, A5, Th65;

        then

        consider H be Subset of X0 such that

         A6: H is open & x0 in H and

         A7: (g .: H) c= G by A3, A4, Th43;

        reconsider H0 = (H /\ C) as Subset of X1 by XBOOLE_1: 17;

        (g .: H0) c= ((g .: H) /\ (g .: C)) & ((g .: H) /\ (g .: C)) c= (g .: H) by RELAT_1: 121, XBOOLE_1: 17;

        then (g .: H0) c= (g .: H) by XBOOLE_1: 1;

        then

         A8: (g .: H0) c= G by A7, XBOOLE_1: 1;

        take H0;

        (g | X1) = (g | C) by A2, Def5;

        then H0 = (H /\ ( [#] X1)) & ((g | X1) .: H0) c= (g .: H0) by RELAT_1: 128;

        hence thesis by A1, A2, A6, A8, TOPS_2: 24, XBOOLE_0:def 4, XBOOLE_1: 1;

      end;

      hence thesis by Th43;

    end;

    theorem :: TMAP_1:75

    

     Th75: X1 is SubSpace of X0 implies for x0 be Point of X0, x1 be Point of X1 st x0 = x1 holds (f | X0) is_continuous_at x0 implies (f | X1) is_continuous_at x1

    proof

      assume

       A1: X1 is SubSpace of X0;

      let x0 be Point of X0, x1 be Point of X1;

      assume

       A2: x0 = x1;

      assume (f | X0) is_continuous_at x0;

      then ((f | X0) | X1) is_continuous_at x1 by A1, A2, Th74;

      hence thesis by A1, Th71;

    end;

    theorem :: TMAP_1:76

    

     Th76: X1 is SubSpace of X0 implies for A be Subset of X0, x0 be Point of X0, x1 be Point of X1 st A c= the carrier of X1 & A is a_neighborhood of x0 & x0 = x1 holds g is_continuous_at x0 iff (g | X1) is_continuous_at x1

    proof

      assume

       A1: X1 is SubSpace of X0;

      let A be Subset of X0, x0 be Point of X0, x1 be Point of X1 such that

       A2: A c= the carrier of X1 and

       A3: A is a_neighborhood of x0 and

       A4: x0 = x1;

      thus g is_continuous_at x0 implies (g | X1) is_continuous_at x1 by A1, A4, Th74;

      thus (g | X1) is_continuous_at x1 implies g is_continuous_at x0

      proof

        assume

         A5: (g | X1) is_continuous_at x1;

        for G be Subset of Y st G is open & (g . x0) in G holds ex H be Subset of X0 st H is open & x0 in H & (g .: H) c= G

        proof

          let G be Subset of Y such that

           A6: G is open and

           A7: (g . x0) in G;

          ((g | X1) . x1) in G by A1, A4, A7, Th65;

          then

          consider H1 be Subset of X1 such that

           A8: H1 is open and

           A9: x1 in H1 and

           A10: ((g | X1) .: H1) c= G by A5, A6, Th43;

          consider V be Subset of X0 such that

           A11: V is open and

           A12: V c= A and

           A13: x0 in V by A3, CONNSP_2: 6;

          reconsider V1 = V as Subset of X1 by A2, A12, XBOOLE_1: 1;

          

           A14: (H1 /\ V1) c= V by XBOOLE_1: 17;

          then

          reconsider H = (H1 /\ V1) as Subset of X0 by XBOOLE_1: 1;

          

           A15: for z be Point of Y holds z in (g .: H) implies z in G

          proof

            set f = (g | X1);

            let z be Point of Y;

            assume z in (g .: H);

            then

            consider y be Point of X0 such that

             A16: y in H and

             A17: z = (g . y) by FUNCT_2: 65;

            y in V by A14, A16;

            then y in A by A12;

            then

             A18: z = (f . y) by A1, A2, A17, Th65;

            (H1 /\ V1) c= H1 by XBOOLE_1: 17;

            then z in (f .: H1) by A16, A18, FUNCT_2: 35;

            hence thesis by A10;

          end;

          take H;

          V1 is open by A1, A11, TOPS_2: 25;

          then (H1 /\ V1) is open by A8;

          hence thesis by A1, A4, A9, A11, A13, A14, A15, SUBSET_1: 2, TSEP_1: 9, XBOOLE_0:def 4;

        end;

        hence thesis by Th43;

      end;

    end;

    theorem :: TMAP_1:77

    

     Th77: X1 is SubSpace of X0 implies for A be Subset of X0, x0 be Point of X0, x1 be Point of X1 st A is open & x0 in A & A c= the carrier of X1 & x0 = x1 holds g is_continuous_at x0 iff (g | X1) is_continuous_at x1

    proof

      assume

       A1: X1 is SubSpace of X0;

      let A be Subset of X0, x0 be Point of X0, x1 be Point of X1 such that

       A2: A is open & x0 in A and

       A3: A c= the carrier of X1 and

       A4: x0 = x1;

      thus g is_continuous_at x0 implies (g | X1) is_continuous_at x1 by A1, A4, Th74;

      thus (g | X1) is_continuous_at x1 implies g is_continuous_at x0

      proof

        assume

         A5: (g | X1) is_continuous_at x1;

        A is a_neighborhood of x0 by A2, CONNSP_2: 3;

        hence thesis by A1, A3, A4, A5, Th76;

      end;

    end;

    theorem :: TMAP_1:78

    X1 is SubSpace of X0 implies for A be Subset of X, x0 be Point of X0, x1 be Point of X1 st A is open & x0 in A & A c= the carrier of X1 & x0 = x1 holds g is_continuous_at x0 iff (g | X1) is_continuous_at x1

    proof

      assume

       A1: X1 is SubSpace of X0;

      let A be Subset of X, x0 be Point of X0, x1 be Point of X1 such that

       A2: A is open and

       A3: x0 in A and

       A4: A c= the carrier of X1 and

       A5: x0 = x1;

      thus g is_continuous_at x0 implies (g | X1) is_continuous_at x1 by A1, A5, Th74;

      thus (g | X1) is_continuous_at x1 implies g is_continuous_at x0

      proof

        the carrier of X1 c= the carrier of X0 by A1, TSEP_1: 4;

        then

        reconsider B = A as Subset of X0 by A4, XBOOLE_1: 1;

        assume

         A6: (g | X1) is_continuous_at x1;

        B is open by A2, TOPS_2: 25;

        hence thesis by A1, A3, A4, A5, A6, Th77;

      end;

    end;

    theorem :: TMAP_1:79

    

     Th79: X1 is open SubSpace of X0 implies for x0 be Point of X0, x1 be Point of X1 st x0 = x1 holds g is_continuous_at x0 iff (g | X1) is_continuous_at x1

    proof

      assume

       A1: X1 is open SubSpace of X0;

      let x0 be Point of X0, x1 be Point of X1;

      assume

       A2: x0 = x1;

      hence g is_continuous_at x0 implies (g | X1) is_continuous_at x1 by A1, Th74;

      thus (g | X1) is_continuous_at x1 implies g is_continuous_at x0

      proof

        reconsider A = the carrier of X1 as Subset of X0 by A1, TSEP_1: 1;

        assume

         A3: (g | X1) is_continuous_at x1;

        A is open by A1, TSEP_1: 16;

        hence thesis by A1, A2, A3, Th77;

      end;

    end;

    theorem :: TMAP_1:80

    X1 is open SubSpace of X & X1 is SubSpace of X0 implies for x0 be Point of X0, x1 be Point of X1 st x0 = x1 holds g is_continuous_at x0 iff (g | X1) is_continuous_at x1

    proof

      assume

       A1: X1 is open SubSpace of X;

      assume

       A2: X1 is SubSpace of X0;

      let x0 be Point of X0, x1 be Point of X1;

      assume

       A3: x0 = x1;

      hence g is_continuous_at x0 implies (g | X1) is_continuous_at x1 by A2, Th74;

      thus (g | X1) is_continuous_at x1 implies g is_continuous_at x0

      proof

        the carrier of X1 c= the carrier of X0 by A2, TSEP_1: 4;

        then

         A4: X1 is open SubSpace of X0 by A1, TSEP_1: 19;

        assume (g | X1) is_continuous_at x1;

        hence thesis by A3, A4, Th79;

      end;

    end;

    theorem :: TMAP_1:81

    

     Th81: the TopStruct of X1 = X0 implies for x0 be Point of X0, x1 be Point of X1 st x0 = x1 holds (g | X1) is_continuous_at x1 implies g is_continuous_at x0

    proof

      reconsider Y1 = the TopStruct of X1 as TopSpace;

      assume

       A1: the TopStruct of X1 = X0;

      then the carrier of X1 c= the carrier of X0;

      then

      reconsider A = the carrier of X1 as Subset of X0;

      A = ( [#] X0) by A1;

      then

       A2: A is open;

      Y1 is SubSpace of X0 by A1, TSEP_1: 2;

      then

       A3: X1 is open SubSpace of X0 by A2, Th7, TSEP_1: 16;

      let x0 be Point of X0, x1 be Point of X1 such that

       A4: x0 = x1;

      assume (g | X1) is_continuous_at x1;

      hence thesis by A4, A3, Th79;

    end;

    theorem :: TMAP_1:82

    

     Th82: for g be continuous Function of X0, Y holds X1 is SubSpace of X0 implies (g | X1) is continuous Function of X1, Y

    proof

      let g be continuous Function of X0, Y;

      assume

       A1: X1 is SubSpace of X0;

      for x1 be Point of X1 holds (g | X1) is_continuous_at x1

      proof

        let x1 be Point of X1;

        consider x0 be Point of X0 such that

         A2: x0 = x1 by A1, Th10;

        g is_continuous_at x0 by Th44;

        hence thesis by A1, A2, Th74;

      end;

      hence thesis by Th44;

    end;

    theorem :: TMAP_1:83

    

     Th83: X1 is SubSpace of X0 & X2 is SubSpace of X1 implies for g be Function of X0, Y holds (g | X1) is continuous Function of X1, Y implies (g | X2) is continuous Function of X2, Y

    proof

      assume

       A1: X1 is SubSpace of X0;

      assume

       A2: X2 is SubSpace of X1;

      let g be Function of X0, Y;

      assume (g | X1) is continuous Function of X1, Y;

      then ((g | X1) | X2) is continuous Function of X2, Y by A2, Th82;

      hence thesis by A1, A2, Th72;

    end;

    registration

      let X;

      cluster ( id X) -> continuous;

      coherence by FUNCT_2: 94;

    end

    definition

      let X be non empty TopSpace, X0 be SubSpace of X;

      :: TMAP_1:def6

      func incl X0 -> Function of X0, X equals (( id X) | X0);

      coherence ;

      correctness ;

    end

    notation

      let X be non empty TopSpace, X0 be SubSpace of X;

      synonym X0 incl X for incl X0;

    end

    theorem :: TMAP_1:84

    for X0 be non empty SubSpace of X, x be Point of X st x in the carrier of X0 holds (( incl X0) . x) = x

    proof

      let X0 be non empty SubSpace of X, x be Point of X;

      assume x in the carrier of X0;

      

      hence (( incl X0) . x) = (( id X) . x) by FUNCT_1: 49

      .= x;

    end;

    theorem :: TMAP_1:85

    for X0 be non empty SubSpace of X, f0 be Function of X0, X st for x be Point of X st x in the carrier of X0 holds x = (f0 . x) holds ( incl X0) = f0

    proof

      let X0 be non empty SubSpace of X, f0 be Function of X0, X;

      assume for x be Point of X st x in the carrier of X0 holds x = (f0 . x);

      then for x be Point of X st x in the carrier of X0 holds (( id X) . x) = (f0 . x);

      hence thesis by Th53;

    end;

    theorem :: TMAP_1:86

    for X0 be non empty SubSpace of X, f be Function of X, Y holds (f | X0) = (f * ( incl X0))

    proof

      let X0 be non empty SubSpace of X, f be Function of X, Y;

      

      thus (f | X0) = ((f * ( id X)) | X0) by FUNCT_2: 17

      .= (f * ( incl X0)) by Th62;

    end;

    theorem :: TMAP_1:87

    for X0 be non empty SubSpace of X holds ( incl X0) is continuous Function of X0, X;

    begin

    reserve X for non empty TopSpace,

H,G for Subset of X;

    definition

      let X;

      let A be Subset of X;

      :: TMAP_1:def7

      func A -extension_of_the_topology_of X -> Subset-Family of X equals { (H \/ (G /\ A)) : H in the topology of X & G in the topology of X };

      coherence

      proof

        set FF = { (H \/ (G /\ A)) : H in the topology of X & G in the topology of X };

        now

          let C be object;

          assume C in FF;

          then ex P,S be Subset of X st C = (P \/ (S /\ A)) & P in the topology of X & S in the topology of X;

          hence C in ( bool the carrier of X);

        end;

        hence thesis by TARSKI:def 3;

      end;

    end

    theorem :: TMAP_1:88

    

     Th88: for A be Subset of X holds the topology of X c= (A -extension_of_the_topology_of X)

    proof

      let A be Subset of X;

      now

        ( {} X) = {} ;

        then

        reconsider G = {} as Subset of X;

        let W be object;

        assume

         A1: W in the topology of X;

        then

        reconsider H = W as Subset of X;

        H = (H \/ (G /\ A)) & G in the topology of X by PRE_TOPC: 1;

        hence W in (A -extension_of_the_topology_of X) by A1;

      end;

      hence thesis by TARSKI:def 3;

    end;

    theorem :: TMAP_1:89

    

     Th89: for A be Subset of X holds { (G /\ A) where G be Subset of X : G in the topology of X } c= (A -extension_of_the_topology_of X)

    proof

      let A be Subset of X;

      now

        ( {} X) = {} ;

        then

        reconsider H = {} as Subset of X;

        let W be object;

        assume W in { (G /\ A) where G be Subset of X : G in the topology of X };

        then

        consider G be Subset of X such that

         A1: W = (G /\ A) & G in the topology of X;

        (G /\ A) = (H \/ (G /\ A)) & H in the topology of X by PRE_TOPC: 1;

        hence W in (A -extension_of_the_topology_of X) by A1;

      end;

      hence thesis by TARSKI:def 3;

    end;

    theorem :: TMAP_1:90

    

     Th90: for A be Subset of X holds for C,D be Subset of X st C in the topology of X & D in { (G /\ A) where G be Subset of X : G in the topology of X } holds (C \/ D) in (A -extension_of_the_topology_of X) & (C /\ D) in (A -extension_of_the_topology_of X)

    proof

      let A be Subset of X;

      let C,D be Subset of X;

      assume

       A1: C in the topology of X;

      assume D in { (G /\ A) where G be Subset of X : G in the topology of X };

      then

      consider G be Subset of X such that

       A2: D = (G /\ A) and

       A3: G in the topology of X;

      thus (C \/ D) in (A -extension_of_the_topology_of X) by A1, A2, A3;

      thus (C /\ D) in (A -extension_of_the_topology_of X)

      proof

        ( {} X) = {} ;

        then

        reconsider H = {} as Subset of X;

        

         A4: (C /\ D) = (H \/ ((C /\ G) /\ A)) & H in the topology of X by A2, PRE_TOPC: 1, XBOOLE_1: 16;

        (C /\ G) in the topology of X by A1, A3, PRE_TOPC:def 1;

        hence thesis by A4;

      end;

    end;

    theorem :: TMAP_1:91

    

     Th91: for A be Subset of X holds A in (A -extension_of_the_topology_of X)

    proof

      let A be Subset of X;

      X is SubSpace of X by TSEP_1: 2;

      then

      reconsider G = the carrier of X as Subset of X by TSEP_1: 1;

      

       A1: G in the topology of X by PRE_TOPC:def 1;

      ( {} X) = {} ;

      then

      reconsider H = {} as Subset of X;

      A = (H \/ (G /\ A)) & H in the topology of X by PRE_TOPC: 1, XBOOLE_1: 28;

      hence thesis by A1;

    end;

    theorem :: TMAP_1:92

    

     Th92: for A be Subset of X holds A in the topology of X iff the topology of X = (A -extension_of_the_topology_of X)

    proof

      let A be Subset of X;

      thus A in the topology of X implies the topology of X = (A -extension_of_the_topology_of X)

      proof

        assume

         A1: A in the topology of X;

        now

          let W be object;

          assume W in (A -extension_of_the_topology_of X);

          then

          consider H,G be Subset of X such that

           A2: W = (H \/ (G /\ A)) and

           A3: H in the topology of X and

           A4: G in the topology of X;

          reconsider H1 = H as Subset of X;

          

           A5: (G /\ A) is open by A1, A4, PRE_TOPC:def 1;

          H1 is open by A3;

          then (H1 \/ (G /\ A)) is open by A5;

          hence W in the topology of X by A2;

        end;

        then

         A6: (A -extension_of_the_topology_of X) c= the topology of X by TARSKI:def 3;

        the topology of X c= (A -extension_of_the_topology_of X) by Th88;

        hence thesis by A6;

      end;

      thus thesis by Th91;

    end;

    definition

      let X be non empty TopSpace, A be Subset of X;

      :: TMAP_1:def8

      func X modified_with_respect_to A -> strict TopSpace equals TopStruct (# the carrier of X, (A -extension_of_the_topology_of X) #);

      coherence

      proof

        set Y = TopStruct (# the carrier of X, (A -extension_of_the_topology_of X) #);

        

         A1: for C,D be Subset of Y st C in the topology of Y & D in the topology of Y holds (C /\ D) in the topology of Y

        proof

          let C,D be Subset of Y;

          assume that

           A2: C in the topology of Y and

           A3: D in the topology of Y;

          consider H1,G1 be Subset of X such that

           A4: C = (H1 \/ (G1 /\ A)) and

           A5: H1 in the topology of X and

           A6: G1 in the topology of X by A2;

          consider H2,G2 be Subset of X such that

           A7: D = (H2 \/ (G2 /\ A)) and

           A8: H2 in the topology of X and

           A9: G2 in the topology of X by A3;

          

           A10: (C /\ D) = ((H1 /\ (H2 \/ (G2 /\ A))) \/ ((G1 /\ A) /\ (H2 \/ (G2 /\ A)))) by A4, A7, XBOOLE_1: 23

          .= (((H1 /\ H2) \/ (H1 /\ (G2 /\ A))) \/ ((G1 /\ A) /\ (H2 \/ (G2 /\ A)))) by XBOOLE_1: 23

          .= (((H1 /\ H2) \/ (H1 /\ (G2 /\ A))) \/ (((G1 /\ A) /\ H2) \/ ((G1 /\ A) /\ (G2 /\ A)))) by XBOOLE_1: 23

          .= (((H1 /\ H2) \/ ((H1 /\ G2) /\ A)) \/ (((G1 /\ A) /\ H2) \/ ((G1 /\ A) /\ (G2 /\ A)))) by XBOOLE_1: 16

          .= (((H1 /\ H2) \/ ((H1 /\ G2) /\ A)) \/ (((G1 /\ A) /\ H2) \/ (G1 /\ ((G2 /\ A) /\ A)))) by XBOOLE_1: 16

          .= (((H1 /\ H2) \/ ((H1 /\ G2) /\ A)) \/ (((G1 /\ A) /\ H2) \/ (G1 /\ (G2 /\ (A /\ A))))) by XBOOLE_1: 16

          .= (((H1 /\ H2) \/ ((H1 /\ G2) /\ A)) \/ ((H2 /\ (G1 /\ A)) \/ ((G1 /\ G2) /\ A))) by XBOOLE_1: 16

          .= (((H1 /\ H2) \/ ((H1 /\ G2) /\ A)) \/ (((H2 /\ G1) /\ A) \/ ((G1 /\ G2) /\ A))) by XBOOLE_1: 16

          .= (((H1 /\ H2) \/ ((H1 /\ G2) /\ A)) \/ (((H2 /\ G1) \/ (G1 /\ G2)) /\ A)) by XBOOLE_1: 23

          .= ((H1 /\ H2) \/ (((H1 /\ G2) /\ A) \/ (((H2 /\ G1) \/ (G1 /\ G2)) /\ A))) by XBOOLE_1: 4

          .= ((H1 /\ H2) \/ (((H1 /\ G2) \/ ((H2 /\ G1) \/ (G1 /\ G2))) /\ A)) by XBOOLE_1: 23

          .= ((H1 /\ H2) \/ ((((H1 /\ G2) \/ (H2 /\ G1)) \/ (G1 /\ G2)) /\ A)) by XBOOLE_1: 4;

          (G1 /\ G2) in the topology of X by A6, A9, PRE_TOPC:def 1;

          then

           A11: (G1 /\ G2) is open;

          

           A12: (H2 /\ G1) is open by A6, A8, PRE_TOPC:def 1;

          (H1 /\ G2) in the topology of X by A5, A9, PRE_TOPC:def 1;

          then (H1 /\ G2) is open;

          then ((H1 /\ G2) \/ (H2 /\ G1)) is open by A12;

          then (((H1 /\ G2) \/ (H2 /\ G1)) \/ (G1 /\ G2)) is open by A11;

          then

           A13: (((H1 /\ G2) \/ (H2 /\ G1)) \/ (G1 /\ G2)) in the topology of X;

          (H1 /\ H2) in the topology of X by A5, A8, PRE_TOPC:def 1;

          hence thesis by A13, A10;

        end;

        

         A14: for FF be Subset-Family of Y st FF c= the topology of Y holds ( union FF) in the topology of Y

        proof

          set SAA = { (G /\ A) where G be Subset of X : G in the topology of X };

          SAA c= (A -extension_of_the_topology_of X) by Th89;

          then

          reconsider SAA as Subset-Family of X by TOPS_2: 2;

          let FF be Subset-Family of Y;

          set AA = { (P \/ (S /\ A)) where P be Subset of X, S be Subset of X : P in the topology of X & S in the topology of X };

          set FF1 = { H where H be Subset of X : H in the topology of X & ex G be Subset of X st G in the topology of X & (H \/ (G /\ A)) in FF };

          set FF2 = { (G /\ A) where G be Subset of X : G in the topology of X & ex H be Subset of X st H in the topology of X & (H \/ (G /\ A)) in FF };

          now

            let W be object;

            assume W in FF1;

            then ex H be Subset of X st W = H & H in the topology of X & ex G be Subset of X st G in the topology of X & (H \/ (G /\ A)) in FF;

            hence W in the topology of X;

          end;

          then

           A15: FF1 c= the topology of X by TARSKI:def 3;

          now

            let W be object;

            assume W in FF2;

            then ex G be Subset of X st W = (G /\ A) & G in the topology of X & ex H be Subset of X st H in the topology of X & (H \/ (G /\ A)) in FF;

            hence W in SAA;

          end;

          then

           A16: FF2 c= SAA by TARSKI:def 3;

          then

          reconsider FF2 as Subset-Family of X by TOPS_2: 2;

          

           A17: ( union FF2) in SAA

          proof

            now

              per cases ;

                suppose

                 A18: A = {} ;

                now

                  let W be object;

                  assume W in { {} };

                  then

                   A19: W = ( {} /\ A) by TARSKI:def 1;

                   {} in the topology of X by PRE_TOPC: 1;

                  hence W in SAA by A19;

                end;

                then

                 A20: { {} } c= SAA by TARSKI:def 3;

                now

                  let W be object;

                  assume W in SAA;

                  then ex G be Subset of X st W = (G /\ A) & G in the topology of X;

                  hence W in { {} } by A18, TARSKI:def 1;

                end;

                then SAA c= { {} } by TARSKI:def 3;

                then

                 A21: SAA = { {} } by A20;

                now

                  per cases by A16, A21, ZFMISC_1: 33;

                    suppose FF2 = { {} };

                    hence ( union FF2) = {} by ZFMISC_1: 25;

                  end;

                    suppose FF2 = {} ;

                    hence ( union FF2) = {} by ZFMISC_1: 2;

                  end;

                end;

                hence thesis by A21, TARSKI:def 1;

              end;

                suppose A <> {} ;

                then

                consider Y be strict non empty SubSpace of X such that

                 A22: A = the carrier of Y by TSEP_1: 10;

                now

                  let W be object;

                  assume W in SAA;

                  then

                  consider G be Subset of X such that

                   A23: W = (G /\ A) and

                   A24: G in the topology of X;

                  reconsider C = (G /\ ( [#] Y)) as Subset of Y;

                  C in the topology of Y by A24, PRE_TOPC:def 4;

                  hence W in the topology of Y by A22, A23;

                end;

                then

                 A25: SAA c= the topology of Y by TARSKI:def 3;

                 A26:

                now

                  let W be object;

                  assume

                   A27: W in the topology of Y;

                  then

                  reconsider C = W as Subset of Y;

                  ex G be Subset of X st G in the topology of X & C = (G /\ ( [#] Y)) by A27, PRE_TOPC:def 4;

                  hence W in SAA by A22;

                end;

                then the topology of Y c= SAA by TARSKI:def 3;

                then

                 A28: the topology of Y = SAA by A25;

                then

                reconsider SS = FF2 as Subset-Family of Y by A16, TOPS_2: 2;

                ( union SS) in the topology of Y by A16, A28, PRE_TOPC:def 1;

                hence thesis by A26;

              end;

            end;

            hence thesis;

          end;

          reconsider FF1 as Subset-Family of X by A15, TOPS_2: 2;

          

           A29: ( union FF1) in the topology of X by A15, PRE_TOPC:def 1;

          now

            let x be object such that

             A30: x in (( union FF1) \/ ( union FF2));

            now

              per cases by A30, XBOOLE_0:def 3;

                suppose x in ( union FF1);

                then

                consider W be set such that

                 A31: x in W and

                 A32: W in FF1 by TARSKI:def 4;

                consider H be Subset of X such that

                 A33: W = H and H in the topology of X and

                 A34: ex G be Subset of X st G in the topology of X & (H \/ (G /\ A)) in FF by A32;

                consider G be Subset of X such that

                 A35: (H \/ (G /\ A)) in FF by A34;

                

                 A36: H c= (H \/ (G /\ A)) by XBOOLE_1: 7;

                (H \/ (G /\ A)) c= ( union FF) by A35, ZFMISC_1: 74;

                then H c= ( union FF) by A36, XBOOLE_1: 1;

                hence x in ( union FF) by A31, A33;

              end;

                suppose x in ( union FF2);

                then

                consider W be set such that

                 A37: x in W and

                 A38: W in FF2 by TARSKI:def 4;

                consider G be Subset of X such that

                 A39: W = (G /\ A) and G in the topology of X and

                 A40: ex H be Subset of X st H in the topology of X & (H \/ (G /\ A)) in FF by A38;

                consider H be Subset of X such that

                 A41: (H \/ (G /\ A)) in FF by A40;

                

                 A42: (G /\ A) c= (H \/ (G /\ A)) by XBOOLE_1: 7;

                (H \/ (G /\ A)) c= ( union FF) by A41, ZFMISC_1: 74;

                then (G /\ A) c= ( union FF) by A42, XBOOLE_1: 1;

                hence x in ( union FF) by A37, A39;

              end;

            end;

            hence x in ( union FF);

          end;

          then

           A43: (( union FF1) \/ ( union FF2)) c= ( union FF) by TARSKI:def 3;

          assume

           A44: FF c= the topology of Y;

          now

            let x be object;

            

             A45: ( union FF1) c= (( union FF1) \/ ( union FF2)) by XBOOLE_1: 7;

            

             A46: ( union FF2) c= (( union FF1) \/ ( union FF2)) by XBOOLE_1: 7;

            assume x in ( union FF);

            then

            consider W be set such that

             A47: x in W and

             A48: W in FF by TARSKI:def 4;

            W in AA by A44, A48;

            then

            consider H,G be Subset of X such that

             A49: W = (H \/ (G /\ A)) and

             A50: H in the topology of X & G in the topology of X;

            (G /\ A) in FF2 by A48, A49, A50;

            then (G /\ A) c= ( union FF2) by ZFMISC_1: 74;

            then

             A51: (G /\ A) c= (( union FF1) \/ ( union FF2)) by A46, XBOOLE_1: 1;

            H in FF1 by A48, A49, A50;

            then H c= ( union FF1) by ZFMISC_1: 74;

            then H c= (( union FF1) \/ ( union FF2)) by A45, XBOOLE_1: 1;

            then (H \/ (G /\ A)) c= (( union FF1) \/ ( union FF2)) by A51, XBOOLE_1: 8;

            hence x in (( union FF1) \/ ( union FF2)) by A47, A49;

          end;

          then ( union FF) c= (( union FF1) \/ ( union FF2)) by TARSKI:def 3;

          then ( union FF) = (( union FF1) \/ ( union FF2)) by A43;

          hence thesis by A29, A17, Th90;

        end;

        the topology of X c= (A -extension_of_the_topology_of X) & the carrier of X in the topology of X by Th88, PRE_TOPC:def 1;

        hence thesis by A14, A1, PRE_TOPC:def 1;

      end;

    end

    registration

      let X be non empty TopSpace, A be Subset of X;

      cluster (X modified_with_respect_to A) -> non empty;

      coherence ;

    end

    reserve A for Subset of X;

    theorem :: TMAP_1:93

    the carrier of (X modified_with_respect_to A) = the carrier of X & the topology of (X modified_with_respect_to A) = (A -extension_of_the_topology_of X);

    theorem :: TMAP_1:94

    

     Th94: for B be Subset of (X modified_with_respect_to A) st B = A holds B is open by Th91;

    theorem :: TMAP_1:95

    

     Th95: for A be Subset of X holds A is open iff the TopStruct of X = (X modified_with_respect_to A) by Th92;

    definition

      let X be non empty TopSpace, A be Subset of X;

      :: TMAP_1:def9

      func modid (X,A) -> Function of X, (X modified_with_respect_to A) equals ( id the carrier of X);

      coherence ;

    end

    theorem :: TMAP_1:96

    

     Th96: for x be Point of X st not x in A holds ( modid (X,A)) is_continuous_at x

    proof

      let x be Point of X;

      assume

       A1: not x in A;

      now

        let W be Subset of (X modified_with_respect_to A);

        assume that

         A2: W is open and

         A3: (( modid (X,A)) . x) in W;

        consider H,G be Subset of X such that

         A4: W = (H \/ (G /\ A)) and

         A5: H in the topology of X and G in the topology of X by A2;

        

         A6: (G /\ A) c= A by XBOOLE_1: 17;

        

         A7: x in H or x in (G /\ A) by A3, A4, XBOOLE_0:def 3;

        thus ex V be Subset of X st V is open & x in V & (( modid (X,A)) .: V) c= W

        proof

          reconsider H as Subset of X;

          take H;

          (( modid (X,A)) .: H) = H by FUNCT_1: 92;

          hence thesis by A1, A4, A5, A7, A6, XBOOLE_1: 7;

        end;

      end;

      hence thesis by Th43;

    end;

    theorem :: TMAP_1:97

    

     Th97: for X0 be non empty SubSpace of X st the carrier of X0 misses A holds for x0 be Point of X0 holds (( modid (X,A)) | X0) is_continuous_at x0

    proof

      let X0 be non empty SubSpace of X;

      assume

       A1: (the carrier of X0 /\ A) = {} ;

      let x0 be Point of X0;

      x0 in the carrier of X0 & the carrier of X0 c= the carrier of X by BORSUK_1: 1;

      then

      reconsider x = x0 as Point of X;

       not x in A by A1, XBOOLE_0:def 4;

      hence thesis by Th58, Th96;

    end;

    theorem :: TMAP_1:98

    

     Th98: for X0 be non empty SubSpace of X st the carrier of X0 = A holds for x0 be Point of X0 holds (( modid (X,A)) | X0) is_continuous_at x0

    proof

      let X0 be non empty SubSpace of X;

      assume

       A1: the carrier of X0 = A;

      let x0 be Point of X0;

      now

        x0 in the carrier of X0 & the carrier of X0 c= the carrier of X by BORSUK_1: 1;

        then

        reconsider x = x0 as Point of X;

        let W be Subset of (X modified_with_respect_to A);

        assume that

         A2: W is open and

         A3: ((( modid (X,A)) | X0) . x0) in W;

        consider H,G be Subset of X such that

         A4: W = (H \/ (G /\ A)) and

         A5: H in the topology of X & G in the topology of X by A2;

        reconsider H, G as Subset of X;

        

         A6: ((H /\ A) \/ (G /\ A)) c= W by A4, XBOOLE_1: 9, XBOOLE_1: 17;

        ((( modid (X,A)) | X0) . x0) = (( id the carrier of X) . x) by FUNCT_1: 49

        .= x;

        then x in H or x in (G /\ A) by A3, A4, XBOOLE_0:def 3;

        then x in (H /\ A) or x in (G /\ A) by A1, XBOOLE_0:def 4;

        then

         A7: x in ((H /\ A) \/ (G /\ A)) by XBOOLE_0:def 3;

        

         A8: ((( modid (X,A)) | X0) .: ((H \/ G) /\ A)) = (( id the carrier of X) .: ((H \/ G) /\ A)) by A1, FUNCT_2: 97, XBOOLE_1: 17

        .= ((H \/ G) /\ A) by FUNCT_1: 92;

        thus ex V be Subset of X0 st V is open & x0 in V & ((( modid (X,A)) | X0) .: V) c= W

        proof

          reconsider V = ((H \/ G) /\ A) as Subset of X0 by A1, XBOOLE_1: 17;

          take V;

          H is open & G is open by A5;

          then

           A9: (H \/ G) is open;

          V = ((H \/ G) /\ ( [#] X0)) by A1;

          hence thesis by A7, A8, A6, A9, TOPS_2: 24, XBOOLE_1: 23;

        end;

      end;

      hence thesis by Th43;

    end;

    theorem :: TMAP_1:99

    

     Th99: for X0 be non empty SubSpace of X st the carrier of X0 misses A holds (( modid (X,A)) | X0) is continuous Function of X0, (X modified_with_respect_to A)

    proof

      let X0 be non empty SubSpace of X;

      assume the carrier of X0 misses A;

      then for x0 be Point of X0 holds (( modid (X,A)) | X0) is_continuous_at x0 by Th97;

      hence thesis by Th44;

    end;

    theorem :: TMAP_1:100

    

     Th100: for X0 be non empty SubSpace of X st the carrier of X0 = A holds (( modid (X,A)) | X0) is continuous Function of X0, (X modified_with_respect_to A)

    proof

      let X0 be non empty SubSpace of X;

      assume the carrier of X0 = A;

      then for x0 be Point of X0 holds (( modid (X,A)) | X0) is_continuous_at x0 by Th98;

      hence thesis by Th44;

    end;

    theorem :: TMAP_1:101

    

     Th101: for A be Subset of X holds A is open iff ( modid (X,A)) is continuous Function of X, (X modified_with_respect_to A)

    proof

      let A be Subset of X;

      thus A is open implies ( modid (X,A)) is continuous Function of X, (X modified_with_respect_to A)

      proof

        reconsider f = ( modid (X,A)) as Function of X, X;

        

         A1: f = ( id X);

        assume A is open;

        then the TopStruct of X = (X modified_with_respect_to A) by Th95;

        hence thesis by A1, Th51;

      end;

      

       A2: ( [#] (X modified_with_respect_to A)) <> {} ;

      thus ( modid (X,A)) is continuous Function of X, (X modified_with_respect_to A) implies A is open

      proof

        set B = (( modid (X,A)) .: A);

        assume

         A3: ( modid (X,A)) is continuous Function of X, (X modified_with_respect_to A);

        B = A by FUNCT_1: 92;

        then

         A4: (( modid (X,A)) " B) = A by FUNCT_2: 94;

        B is open by Th94, FUNCT_1: 92;

        hence thesis by A2, A3, A4, TOPS_2: 43;

      end;

    end;

    definition

      let X be non empty TopSpace, X0 be SubSpace of X;

      :: TMAP_1:def10

      func X modified_with_respect_to X0 -> strict TopSpace means

      : Def10: for A be Subset of X st A = the carrier of X0 holds it = (X modified_with_respect_to A);

      existence

      proof

        reconsider B = the carrier of X0 as Subset of X by TSEP_1: 1;

        take (X modified_with_respect_to B);

        thus thesis;

      end;

      uniqueness

      proof

        reconsider C = the carrier of X0 as Subset of X by TSEP_1: 1;

        let Y1,Y2 be strict TopSpace such that

         A1: for A be Subset of X st A = the carrier of X0 holds Y1 = (X modified_with_respect_to A) and

         A2: for A be Subset of X st A = the carrier of X0 holds Y2 = (X modified_with_respect_to A);

        Y1 = (X modified_with_respect_to C) by A1;

        hence thesis by A2;

      end;

    end

    registration

      let X be non empty TopSpace, X0 be SubSpace of X;

      cluster (X modified_with_respect_to X0) -> non empty;

      coherence

      proof

        ( [#] X0) c= ( [#] X) by PRE_TOPC:def 4;

        then

        reconsider O = ( [#] X0) as Subset of X;

        (X modified_with_respect_to X0) = (X modified_with_respect_to O) by Def10;

        hence thesis;

      end;

    end

    reserve X0 for non empty SubSpace of X;

    theorem :: TMAP_1:102

    

     Th102: the carrier of (X modified_with_respect_to X0) = the carrier of X & for A be Subset of X st A = the carrier of X0 holds the topology of (X modified_with_respect_to X0) = (A -extension_of_the_topology_of X)

    proof

      set Y = (X modified_with_respect_to X0);

      reconsider A = the carrier of X0 as Subset of X by TSEP_1: 1;

      

       A1: Y = (X modified_with_respect_to A) by Def10;

      hence the carrier of (X modified_with_respect_to X0) = the carrier of X;

      thus thesis by A1;

    end;

    theorem :: TMAP_1:103

    for Y0 be SubSpace of (X modified_with_respect_to X0) st the carrier of Y0 = the carrier of X0 holds Y0 is open SubSpace of (X modified_with_respect_to X0)

    proof

      let Y0 be SubSpace of (X modified_with_respect_to X0);

      assume

       A1: the carrier of Y0 = the carrier of X0;

      reconsider A = the carrier of X0 as Subset of X by TSEP_1: 1;

      set Y = (X modified_with_respect_to X0);

      reconsider B = the carrier of Y0 as Subset of Y by TSEP_1: 1;

      Y = (X modified_with_respect_to A) by Def10;

      then B is open by A1, Th94;

      hence thesis by TSEP_1: 16;

    end;

    theorem :: TMAP_1:104

    X0 is open SubSpace of X iff the TopStruct of X = (X modified_with_respect_to X0)

    proof

      thus X0 is open SubSpace of X implies the TopStruct of X = (X modified_with_respect_to X0)

      proof

        reconsider A = the carrier of X0 as Subset of X by TSEP_1: 1;

        assume X0 is open SubSpace of X;

        then A is open by TSEP_1:def 1;

        then the TopStruct of X = (X modified_with_respect_to A) by Th95;

        hence thesis by Def10;

      end;

      thus the TopStruct of X = (X modified_with_respect_to X0) implies X0 is open SubSpace of X

      proof

        assume

         A1: the TopStruct of X = (X modified_with_respect_to X0);

        now

          let A be Subset of X;

          assume A = the carrier of X0;

          then the TopStruct of X = (X modified_with_respect_to A) by A1, Def10;

          hence A is open by Th95;

        end;

        hence thesis by TSEP_1:def 1;

      end;

    end;

    definition

      let X be non empty TopSpace, X0 be SubSpace of X;

      :: TMAP_1:def11

      func modid (X,X0) -> Function of X, (X modified_with_respect_to X0) means

      : Def11: for A be Subset of X st A = the carrier of X0 holds it = ( modid (X,A));

      existence

      proof

        reconsider B = the carrier of X0 as Subset of X by TSEP_1: 1;

        reconsider F = ( modid (X,B)) as Function of X, (X modified_with_respect_to X0) by Def10;

        take F;

        thus thesis;

      end;

      uniqueness

      proof

        reconsider C = the carrier of X0 as Subset of X by TSEP_1: 1;

        let F1,F2 be Function of X, (X modified_with_respect_to X0) such that

         A1: for A be Subset of X st A = the carrier of X0 holds F1 = ( modid (X,A)) and

         A2: for A be Subset of X st A = the carrier of X0 holds F2 = ( modid (X,A));

        F1 = ( modid (X,C)) by A1;

        hence thesis by A2;

      end;

    end

    theorem :: TMAP_1:105

    ( modid (X,X0)) = ( id X)

    proof

      reconsider A = the carrier of X0 as Subset of X by TSEP_1: 1;

      ( modid (X,A)) = ( modid (X,X0)) by Def11;

      hence thesis;

    end;

    theorem :: TMAP_1:106

    

     Th106: for X0,X1 be non empty SubSpace of X st X0 misses X1 holds for x1 be Point of X1 holds (( modid (X,X0)) | X1) is_continuous_at x1

    proof

      let X0,X1 be non empty SubSpace of X;

      reconsider A = the carrier of X0 as Subset of X by TSEP_1: 1;

      reconsider f = (( modid (X,A)) | X1) as Function of X1, (X modified_with_respect_to X0) by Def10;

      assume

       A1: X0 misses X1;

      let x1 be Point of X1;

      the carrier of X1 misses A by A1, TSEP_1:def 3;

      then

       A2: (( modid (X,A)) | X1) is_continuous_at x1 by Th97;

      now

        let W be Subset of (X modified_with_respect_to X0);

        reconsider W0 = W as Subset of (X modified_with_respect_to A) by Th102;

        assume that

         A3: W is open and

         A4: (f . x1) in W;

        W in the topology of (X modified_with_respect_to X0) by A3;

        then W in (A -extension_of_the_topology_of X) by Th102;

        then

         A5: W0 is open;

        thus ex V be Subset of X1 st V is open & x1 in V & (f .: V) c= W

        proof

          consider V be Subset of X1 such that

           A6: V is open & x1 in V & ((( modid (X,A)) | X1) .: V) c= W0 by A2, A4, A5, Th43;

          take V;

          thus thesis by A6;

        end;

      end;

      then f is_continuous_at x1 by Th43;

      hence thesis by Def11;

    end;

    theorem :: TMAP_1:107

    

     Th107: for X0 be non empty SubSpace of X holds for x0 be Point of X0 holds (( modid (X,X0)) | X0) is_continuous_at x0

    proof

      let X0 be non empty SubSpace of X;

      reconsider A = the carrier of X0 as Subset of X by TSEP_1: 1;

      reconsider f = (( modid (X,A)) | X0) as Function of X0, (X modified_with_respect_to X0) by Def10;

      let x0 be Point of X0;

      

       A1: (( modid (X,A)) | X0) is_continuous_at x0 by Th98;

      now

        let W be Subset of (X modified_with_respect_to X0);

        reconsider W0 = W as Subset of (X modified_with_respect_to A) by Th102;

        assume that

         A2: W is open and

         A3: (f . x0) in W;

        W in the topology of (X modified_with_respect_to X0) by A2;

        then W in (A -extension_of_the_topology_of X) by Th102;

        then

         A4: W0 is open;

        thus ex V be Subset of X0 st V is open & x0 in V & (f .: V) c= W

        proof

          consider V be Subset of X0 such that

           A5: V is open & x0 in V & ((( modid (X,A)) | X0) .: V) c= W0 by A1, A3, A4, Th43;

          take V;

          thus thesis by A5;

        end;

      end;

      then f is_continuous_at x0 by Th43;

      hence thesis by Def11;

    end;

    theorem :: TMAP_1:108

    for X0,X1 be non empty SubSpace of X st X0 misses X1 holds (( modid (X,X0)) | X1) is continuous Function of X1, (X modified_with_respect_to X0)

    proof

      let X0,X1 be non empty SubSpace of X;

      assume X0 misses X1;

      then for x1 be Point of X1 holds (( modid (X,X0)) | X1) is_continuous_at x1 by Th106;

      hence thesis by Th44;

    end;

    theorem :: TMAP_1:109

    for X0 be non empty SubSpace of X holds (( modid (X,X0)) | X0) is continuous Function of X0, (X modified_with_respect_to X0)

    proof

      let X0 be non empty SubSpace of X;

      for x0 be Point of X0 holds (( modid (X,X0)) | X0) is_continuous_at x0 by Th107;

      hence thesis by Th44;

    end;

    theorem :: TMAP_1:110

    for X0 be SubSpace of X holds X0 is open SubSpace of X iff ( modid (X,X0)) is continuous Function of X, (X modified_with_respect_to X0)

    proof

      let X0 be SubSpace of X;

      reconsider A = the carrier of X0 as Subset of X by TSEP_1: 1;

      thus X0 is open SubSpace of X implies ( modid (X,X0)) is continuous Function of X, (X modified_with_respect_to X0)

      proof

        assume X0 is open SubSpace of X;

        then

         A1: A is open by TSEP_1: 16;

        (X modified_with_respect_to X0) = (X modified_with_respect_to A) & ( modid (X,X0)) = ( modid (X,A)) by Def10, Def11;

        hence thesis by A1, Th101;

      end;

      thus ( modid (X,X0)) is continuous Function of X, (X modified_with_respect_to X0) implies X0 is open SubSpace of X

      proof

        assume

         A2: ( modid (X,X0)) is continuous Function of X, (X modified_with_respect_to X0);

        (X modified_with_respect_to X0) = (X modified_with_respect_to A) & ( modid (X,X0)) = ( modid (X,A)) by Def10, Def11;

        then A is open by A2, Th101;

        hence thesis by TSEP_1: 16;

      end;

    end;

    begin

    reserve X,Y for non empty TopSpace;

    theorem :: TMAP_1:111

    

     Th111: for X1,X2 be non empty SubSpace of X, g be Function of (X1 union X2), Y holds for x1 be Point of X1, x2 be Point of X2, x be Point of (X1 union X2) st x = x1 & x = x2 holds g is_continuous_at x iff (g | X1) is_continuous_at x1 & (g | X2) is_continuous_at x2

    proof

      let X1,X2 be non empty SubSpace of X, g be Function of (X1 union X2), Y;

      let x1 be Point of X1, x2 be Point of X2, x be Point of (X1 union X2) such that

       A1: x = x1 and

       A2: x = x2;

      

       A3: X2 is SubSpace of (X1 union X2) by TSEP_1: 22;

      

       A4: X1 is SubSpace of (X1 union X2) by TSEP_1: 22;

      hence g is_continuous_at x implies (g | X1) is_continuous_at x1 & (g | X2) is_continuous_at x2 by A1, A2, A3, Th74;

      thus (g | X1) is_continuous_at x1 & (g | X2) is_continuous_at x2 implies g is_continuous_at x

      proof

        assume that

         A5: (g | X1) is_continuous_at x1 and

         A6: (g | X2) is_continuous_at x2;

        for G be a_neighborhood of (g . x) holds ex H be a_neighborhood of x st (g .: H) c= G

        proof

          let G be a_neighborhood of (g . x);

          (g . x) = ((g | X1) . x1) by A1, A4, Th65;

          then

          consider H1 be a_neighborhood of x1 such that

           A7: ((g | X1) .: H1) c= G by A5;

          (g . x) = ((g | X2) . x2) by A2, A3, Th65;

          then

          consider H2 be a_neighborhood of x2 such that

           A8: ((g | X2) .: H2) c= G by A6;

          the carrier of X2 c= the carrier of (X1 union X2) by A3, TSEP_1: 4;

          then

          reconsider S2 = H2 as Subset of (X1 union X2) by XBOOLE_1: 1;

          (g .: S2) c= G by A3, A8, Th68;

          then

           A9: S2 c= (g " G) by FUNCT_2: 95;

          the carrier of X1 c= the carrier of (X1 union X2) by A4, TSEP_1: 4;

          then

          reconsider S1 = H1 as Subset of (X1 union X2) by XBOOLE_1: 1;

          consider H be a_neighborhood of x such that

           A10: H c= (H1 \/ H2) by A1, A2, Th16;

          take H;

          (g .: S1) c= G by A4, A7, Th68;

          then S1 c= (g " G) by FUNCT_2: 95;

          then (S1 \/ S2) c= (g " G) by A9, XBOOLE_1: 8;

          then H c= (g " G) by A10, XBOOLE_1: 1;

          hence thesis by FUNCT_2: 95;

        end;

        hence thesis;

      end;

    end;

    theorem :: TMAP_1:112

    for f be Function of X, Y, X1,X2 be non empty SubSpace of X holds for x be Point of (X1 union X2), x1 be Point of X1, x2 be Point of X2 st x = x1 & x = x2 holds (f | (X1 union X2)) is_continuous_at x iff (f | X1) is_continuous_at x1 & (f | X2) is_continuous_at x2

    proof

      let f be Function of X, Y, X1,X2 be non empty SubSpace of X;

      

       A1: X1 is SubSpace of (X1 union X2) & X2 is SubSpace of (X1 union X2) by TSEP_1: 22;

      let x be Point of (X1 union X2), x1 be Point of X1, x2 be Point of X2 such that

       A2: x = x1 & x = x2;

      thus (f | (X1 union X2)) is_continuous_at x implies (f | X1) is_continuous_at x1 & (f | X2) is_continuous_at x2 by A2, A1, Th75;

      thus (f | X1) is_continuous_at x1 & (f | X2) is_continuous_at x2 implies (f | (X1 union X2)) is_continuous_at x

      proof

        set g = (f | (X1 union X2));

        assume

         A3: (f | X1) is_continuous_at x1 & (f | X2) is_continuous_at x2;

        (g | X1) = (f | X1) & (g | X2) = (f | X2) by A1, Th70;

        hence thesis by A2, A3, Th111;

      end;

    end;

    theorem :: TMAP_1:113

    for f be Function of X, Y, X1,X2 be non empty SubSpace of X st X = (X1 union X2) holds for x be Point of X, x1 be Point of X1, x2 be Point of X2 st x = x1 & x = x2 holds f is_continuous_at x iff (f | X1) is_continuous_at x1 & (f | X2) is_continuous_at x2

    proof

      let f be Function of X, Y, X1,X2 be non empty SubSpace of X such that

       A1: X = (X1 union X2);

      let x be Point of X, x1 be Point of X1, x2 be Point of X2;

      assume that

       A2: x = x1 and

       A3: x = x2;

      thus f is_continuous_at x implies (f | X1) is_continuous_at x1 & (f | X2) is_continuous_at x2 by A2, A3, Th58;

      thus (f | X1) is_continuous_at x1 & (f | X2) is_continuous_at x2 implies f is_continuous_at x

      proof

        assume that

         A4: (f | X1) is_continuous_at x1 and

         A5: (f | X2) is_continuous_at x2;

        for G be a_neighborhood of (f . x) holds ex H be a_neighborhood of x st (f .: H) c= G

        proof

          let G be a_neighborhood of (f . x);

          (f . x) = ((f | X1) . x1) by A2, FUNCT_1: 49;

          then

          consider H1 be a_neighborhood of x1 such that

           A6: ((f | X1) .: H1) c= G by A4;

          the carrier of X1 c= the carrier of X by BORSUK_1: 1;

          then

          reconsider S1 = H1 as Subset of X by XBOOLE_1: 1;

          (f . x) = ((f | X2) . x2) by A3, FUNCT_1: 49;

          then

          consider H2 be a_neighborhood of x2 such that

           A7: ((f | X2) .: H2) c= G by A5;

          the carrier of X2 c= the carrier of X by BORSUK_1: 1;

          then

          reconsider S2 = H2 as Subset of X by XBOOLE_1: 1;

          (f .: S2) c= G by A7, FUNCT_2: 97;

          then

           A8: S2 c= (f " G) by FUNCT_2: 95;

          consider H be a_neighborhood of x such that

           A9: H c= (H1 \/ H2) by A1, A2, A3, Th16;

          take H;

          (f .: S1) c= G by A6, FUNCT_2: 97;

          then S1 c= (f " G) by FUNCT_2: 95;

          then (S1 \/ S2) c= (f " G) by A8, XBOOLE_1: 8;

          then H c= (f " G) by A9, XBOOLE_1: 1;

          hence thesis by FUNCT_2: 95;

        end;

        hence thesis;

      end;

    end;

    reserve X1,X2 for non empty SubSpace of X;

    theorem :: TMAP_1:114

    

     Th114: (X1,X2) are_weakly_separated implies for g be Function of (X1 union X2), Y holds g is continuous Function of (X1 union X2), Y iff (g | X1) is continuous Function of X1, Y & (g | X2) is continuous Function of X2, Y

    proof

      assume

       A1: (X1,X2) are_weakly_separated ;

      let g be Function of (X1 union X2), Y;

      

       A2: X2 is SubSpace of (X1 union X2) by TSEP_1: 22;

      

       A3: X1 is SubSpace of (X1 union X2) by TSEP_1: 22;

      hence g is continuous Function of (X1 union X2), Y implies (g | X1) is continuous Function of X1, Y & (g | X2) is continuous Function of X2, Y by A2, Th82;

      thus (g | X1) is continuous Function of X1, Y & (g | X2) is continuous Function of X2, Y implies g is continuous Function of (X1 union X2), Y

      proof

        assume that

         A4: (g | X1) is continuous Function of X1, Y and

         A5: (g | X2) is continuous Function of X2, Y;

        for x be Point of (X1 union X2) holds g is_continuous_at x

        proof

          set X0 = (X1 union X2);

          let x be Point of (X1 union X2);

          

           A6: X1 meets X2 implies g is_continuous_at x

          proof

            assume

             A7: X1 meets X2;

             A8:

            now

              assume

               A9: ( not X1 is SubSpace of X2) & not X2 is SubSpace of X1;

              then

              consider Y1,Y2 be open non empty SubSpace of X such that

               A10: (Y1 meet X0) is SubSpace of X1 and

               A11: (Y2 meet X0) is SubSpace of X2 and

               A12: X0 is SubSpace of (Y1 union Y2) or ex Z be closed non empty SubSpace of X st the TopStruct of X = ((Y1 union Y2) union Z) & (Z meet X0) is SubSpace of (X1 meet X2) by A1, A7, TSEP_1: 89;

              

               A13: Y2 meets X0 implies (Y2 meet X0) is open SubSpace of X0 by Th39;

              

               A14: Y1 meets X0 implies (Y1 meet X0) is open SubSpace of X0 by Th39;

               A15:

              now

                X is SubSpace of X by TSEP_1: 2;

                then

                reconsider X12 = the TopStruct of X as SubSpace of X by Th6;

                assume

                 A16: not X0 is SubSpace of (Y1 union Y2);

                then

                consider Z be closed non empty SubSpace of X such that

                 A17: the TopStruct of X = ((Y1 union Y2) union Z) and

                 A18: (Z meet X0) is SubSpace of (X1 meet X2) by A12;

                the carrier of X0 c= the carrier of X12 by BORSUK_1: 1;

                then

                 A19: X0 is SubSpace of X12 by TSEP_1: 4;

                then X12 meets X0 by Th17;

                then

                 A20: (((Y1 union Y2) union Z) meet X0) = the TopStruct of X0 by A17, A19, TSEP_1: 28;

                

                 A21: Y1 meets X0 & Y2 meets X0 by A7, A9, A10, A11, A17, A18, Th32;

                 A22:

                now

                   A23:

                  now

                    given x2 be Point of (Y2 meet X0) such that

                     A24: x2 = x;

                    (g | (Y2 meet X0)) is continuous by A2, A5, A11, Th83;

                    then (g | (Y2 meet X0)) is_continuous_at x2;

                    hence thesis by A7, A9, A10, A11, A13, A17, A18, A24, Th32, Th79;

                  end;

                   A25:

                  now

                    given x1 be Point of (Y1 meet X0) such that

                     A26: x1 = x;

                    (g | (Y1 meet X0)) is continuous by A3, A4, A10, Th83;

                    then (g | (Y1 meet X0)) is_continuous_at x1;

                    hence thesis by A7, A9, A10, A11, A14, A17, A18, A26, Th32, Th79;

                  end;

                  assume

                   A27: ex x12 be Point of ((Y1 union Y2) meet X0) st x12 = x;

                  ((Y1 union Y2) meet X0) = ((Y1 meet X0) union (Y2 meet X0)) by A21, TSEP_1: 32;

                  hence thesis by A27, A25, A23, Th11;

                end;

                 A28:

                now

                  given x0 be Point of (Z meet X0) such that

                   A29: x0 = x;

                  consider x00 be Point of (X1 meet X2) such that

                   A30: x00 = x0 by A18, Th10;

                  consider x1 be Point of X1 such that

                   A31: x1 = x00 by A7, Th12;

                  consider x2 be Point of X2 such that

                   A32: x2 = x00 by A7, Th12;

                  (g | X1) is_continuous_at x1 & (g | X2) is_continuous_at x2 by A4, A5, Th44;

                  hence thesis by A29, A30, A31, A32, Th111;

                end;

                (Y1 union Y2) meets X0 & Z meets X0 by A7, A9, A10, A11, A16, A17, A18, Th33;

                then (((Y1 union Y2) meet X0) union (Z meet X0)) = the TopStruct of X0 by A20, TSEP_1: 32;

                hence thesis by A22, A28, Th11;

              end;

              now

                assume

                 A33: X0 is SubSpace of (Y1 union Y2);

                then

                 A34: Y1 meets X0 by A9, A10, A11, Th31;

                 A35:

                now

                  given x2 be Point of (Y2 meet X0) such that

                   A36: x2 = x;

                  (g | (Y2 meet X0)) is continuous by A2, A5, A11, Th83;

                  then (g | (Y2 meet X0)) is_continuous_at x2;

                  hence thesis by A9, A10, A11, A13, A33, A36, Th31, Th79;

                end;

                 A37:

                now

                  given x1 be Point of (Y1 meet X0) such that

                   A38: x1 = x;

                  (g | (Y1 meet X0)) is continuous by A3, A4, A10, Th83;

                  then (g | (Y1 meet X0)) is_continuous_at x1;

                  hence thesis by A9, A10, A11, A14, A33, A38, Th31, Th79;

                end;

                Y1 is SubSpace of (Y1 union Y2) by TSEP_1: 22;

                then (Y1 union Y2) meets X0 by A34, Th18;

                then

                 A39: ((Y1 union Y2) meet X0) = X0 by A33, TSEP_1: 28;

                Y2 meets X0 by A9, A10, A11, A33, Th31;

                then ((Y1 meet X0) union (Y2 meet X0)) = X0 by A34, A39, TSEP_1: 32;

                hence thesis by A37, A35, Th11;

              end;

              hence thesis by A15;

            end;

            now

               A40:

              now

                assume X2 is SubSpace of X1;

                then

                 A41: the TopStruct of X1 = X0 by TSEP_1: 23;

                then

                reconsider x1 = x as Point of X1;

                (g | X1) is_continuous_at x1 by A4, Th44;

                hence thesis by A41, Th81;

              end;

               A42:

              now

                assume X1 is SubSpace of X2;

                then

                 A43: the TopStruct of X2 = X0 by TSEP_1: 23;

                then

                reconsider x2 = x as Point of X2;

                (g | X2) is_continuous_at x2 by A5, Th44;

                hence thesis by A43, Th81;

              end;

              assume X1 is SubSpace of X2 or X2 is SubSpace of X1;

              hence thesis by A42, A40;

            end;

            hence thesis by A8;

          end;

          X1 misses X2 implies g is_continuous_at x

          proof

            assume X1 misses X2;

            then (X1,X2) are_separated by A1, TSEP_1: 78;

            then

            consider Y1,Y2 be open non empty SubSpace of X such that

             A44: X1 is SubSpace of Y1 and

             A45: X2 is SubSpace of Y2 and

             A46: Y1 misses Y2 or (Y1 meet Y2) misses X0 by TSEP_1: 77;

            Y2 misses X1 by A44, A45, A46, Th30;

            then

             A47: X2 is open SubSpace of X0 by A45, Th41;

             A48:

            now

              given x2 be Point of X2 such that

               A49: x2 = x;

              (g | X2) is_continuous_at x2 by A5, Th44;

              hence thesis by A47, A49, Th79;

            end;

            Y1 misses X2 by A44, A45, A46, Th30;

            then

             A50: X1 is open SubSpace of X0 by A44, Th41;

            now

              given x1 be Point of X1 such that

               A51: x1 = x;

              (g | X1) is_continuous_at x1 by A4, Th44;

              hence thesis by A50, A51, Th79;

            end;

            hence thesis by A48, Th11;

          end;

          hence thesis by A6;

        end;

        hence thesis by Th44;

      end;

    end;

    theorem :: TMAP_1:115

    

     Th115: for X1,X2 be closed non empty SubSpace of X holds for g be Function of (X1 union X2), Y holds g is continuous Function of (X1 union X2), Y iff (g | X1) is continuous Function of X1, Y & (g | X2) is continuous Function of X2, Y

    proof

      let X1,X2 be closed non empty SubSpace of X;

      let g be Function of (X1 union X2), Y;

      (X1,X2) are_weakly_separated by TSEP_1: 80;

      hence thesis by Th114;

    end;

    theorem :: TMAP_1:116

    

     Th116: for X1,X2 be open non empty SubSpace of X holds for g be Function of (X1 union X2), Y holds g is continuous Function of (X1 union X2), Y iff (g | X1) is continuous Function of X1, Y & (g | X2) is continuous Function of X2, Y

    proof

      let X1,X2 be open non empty SubSpace of X;

      let g be Function of (X1 union X2), Y;

      (X1,X2) are_weakly_separated by TSEP_1: 81;

      hence thesis by Th114;

    end;

    theorem :: TMAP_1:117

    

     Th117: (X1,X2) are_weakly_separated implies for f be Function of X, Y holds (f | (X1 union X2)) is continuous Function of (X1 union X2), Y iff (f | X1) is continuous Function of X1, Y & (f | X2) is continuous Function of X2, Y

    proof

      assume

       A1: (X1,X2) are_weakly_separated ;

      let f be Function of X, Y;

      

       A2: X2 is SubSpace of (X1 union X2) by TSEP_1: 22;

      then

       A3: ((f | (X1 union X2)) | X2) = (f | X2) by Th71;

      

       A4: X1 is SubSpace of (X1 union X2) by TSEP_1: 22;

      then

       A5: ((f | (X1 union X2)) | X1) = (f | X1) by Th71;

      hence (f | (X1 union X2)) is continuous Function of (X1 union X2), Y implies (f | X1) is continuous Function of X1, Y & (f | X2) is continuous Function of X2, Y by A4, A2, A3, Th82;

      thus thesis by A1, A5, A3, Th114;

    end;

    theorem :: TMAP_1:118

    for f be Function of X, Y, X1,X2 be closed non empty SubSpace of X holds (f | (X1 union X2)) is continuous Function of (X1 union X2), Y iff (f | X1) is continuous Function of X1, Y & (f | X2) is continuous Function of X2, Y

    proof

      let f be Function of X, Y, X1,X2 be closed non empty SubSpace of X;

      (X1,X2) are_weakly_separated by TSEP_1: 80;

      hence thesis by Th117;

    end;

    theorem :: TMAP_1:119

    for f be Function of X, Y, X1,X2 be open non empty SubSpace of X holds (f | (X1 union X2)) is continuous Function of (X1 union X2), Y iff (f | X1) is continuous Function of X1, Y & (f | X2) is continuous Function of X2, Y

    proof

      let f be Function of X, Y, X1,X2 be open non empty SubSpace of X;

      (X1,X2) are_weakly_separated by TSEP_1: 81;

      hence thesis by Th117;

    end;

    theorem :: TMAP_1:120

    

     Th120: for f be Function of X, Y, X1,X2 be non empty SubSpace of X st X = (X1 union X2) & (X1,X2) are_weakly_separated holds f is continuous Function of X, Y iff (f | X1) is continuous Function of X1, Y & (f | X2) is continuous Function of X2, Y

    proof

      let f be Function of X, Y, X1,X2 be non empty SubSpace of X such that

       A1: X = (X1 union X2) and

       A2: (X1,X2) are_weakly_separated ;

      thus f is continuous Function of X, Y implies (f | X1) is continuous Function of X1, Y & (f | X2) is continuous Function of X2, Y;

      assume (f | X1) is continuous Function of X1, Y & (f | X2) is continuous Function of X2, Y;

      then (f | (X1 union X2)) is continuous Function of (X1 union X2), Y by A2, Th117;

      hence thesis by A1, Th54;

    end;

    theorem :: TMAP_1:121

    

     Th121: for f be Function of X, Y, X1,X2 be closed non empty SubSpace of X st X = (X1 union X2) holds f is continuous Function of X, Y iff (f | X1) is continuous Function of X1, Y & (f | X2) is continuous Function of X2, Y

    proof

      let f be Function of X, Y, X1,X2 be closed non empty SubSpace of X such that

       A1: X = (X1 union X2);

      (X1,X2) are_weakly_separated by TSEP_1: 80;

      hence thesis by A1, Th120;

    end;

    theorem :: TMAP_1:122

    

     Th122: for f be Function of X, Y, X1,X2 be open non empty SubSpace of X st X = (X1 union X2) holds f is continuous Function of X, Y iff (f | X1) is continuous Function of X1, Y & (f | X2) is continuous Function of X2, Y

    proof

      let f be Function of X, Y, X1,X2 be open non empty SubSpace of X such that

       A1: X = (X1 union X2);

      (X1,X2) are_weakly_separated by TSEP_1: 81;

      hence thesis by A1, Th120;

    end;

    theorem :: TMAP_1:123

    

     Th123: (X1,X2) are_separated iff X1 misses X2 & for Y be non empty TopSpace, g be Function of (X1 union X2), Y st (g | X1) is continuous Function of X1, Y & (g | X2) is continuous Function of X2, Y holds g is continuous Function of (X1 union X2), Y

    proof

      thus (X1,X2) are_separated implies X1 misses X2 & for Y be non empty TopSpace, g be Function of (X1 union X2), Y st (g | X1) is continuous Function of X1, Y & (g | X2) is continuous Function of X2, Y holds g is continuous Function of (X1 union X2), Y

      proof

        assume

         A1: (X1,X2) are_separated ;

        hence X1 misses X2 by TSEP_1: 63;

        (X1,X2) are_weakly_separated by A1, TSEP_1: 78;

        hence thesis by Th114;

      end;

      thus X1 misses X2 & (for Y be non empty TopSpace, g be Function of (X1 union X2), Y st (g | X1) is continuous Function of X1, Y & (g | X2) is continuous Function of X2, Y holds g is continuous Function of (X1 union X2), Y) implies (X1,X2) are_separated

      proof

        reconsider Y1 = X1, Y2 = X2 as SubSpace of (X1 union X2) by TSEP_1: 22;

        reconsider A2 = the carrier of X2 as Subset of X by TSEP_1: 1;

        reconsider A1 = the carrier of X1 as Subset of X by TSEP_1: 1;

        

         A2: the carrier of (X1 union X2) = (A1 \/ A2) by TSEP_1:def 2;

        then

        reconsider C1 = A1 as Subset of (X1 union X2) by XBOOLE_1: 7;

        reconsider C2 = A2 as Subset of (X1 union X2) by A2, XBOOLE_1: 7;

        

         A3: ( Cl C1) = (( Cl A1) /\ ( [#] (X1 union X2))) by PRE_TOPC: 17;

        

         A4: ( Cl C2) = (( Cl A2) /\ ( [#] (X1 union X2))) by PRE_TOPC: 17;

        assume X1 misses X2;

        then

         A5: C1 misses C2 by TSEP_1:def 3;

        assume

         A6: for Y be non empty TopSpace, g be Function of (X1 union X2), Y st (g | X1) is continuous Function of X1, Y & (g | X2) is continuous Function of X2, Y holds g is continuous Function of (X1 union X2), Y;

        assume (X1,X2) are_not_separated ;

        then

         A7: ex A10,A20 be Subset of X st A10 = the carrier of X1 & A20 = the carrier of X2 & (A10,A20) are_not_separated by TSEP_1:def 6;

         A8:

        now

          assume

           A9: (C1,C2) are_separated ;

          then (( Cl A1) /\ ( [#] (X1 union X2))) misses A2 by A3, CONNSP_1:def 1;

          then ((( Cl A1) /\ ( [#] (X1 union X2))) /\ A2) = {} ;

          then

           A10: ((( Cl A1) /\ A2) /\ ( [#] (X1 union X2))) = {} by XBOOLE_1: 16;

          A1 misses (( Cl A2) /\ ( [#] (X1 union X2))) by A4, A9, CONNSP_1:def 1;

          then (A1 /\ (( Cl A2) /\ ( [#] (X1 union X2)))) = {} ;

          then

           A11: ((A1 /\ ( Cl A2)) /\ ( [#] (X1 union X2))) = {} by XBOOLE_1: 16;

          C1 c= ( [#] (X1 union X2)) & (A1 /\ ( Cl A2)) c= A1 by XBOOLE_1: 17;

          then (A1 /\ ( Cl A2)) = {} by A11, XBOOLE_1: 1, XBOOLE_1: 28;

          then

           A12: A1 misses ( Cl A2);

          C2 c= ( [#] (X1 union X2)) & (( Cl A1) /\ A2) c= A2 by XBOOLE_1: 17;

          then (( Cl A1) /\ A2) = {} by A10, XBOOLE_1: 1, XBOOLE_1: 28;

          then ( Cl A1) misses A2;

          hence contradiction by A7, A12, CONNSP_1:def 1;

        end;

        now

          per cases by A8, A5, TSEP_1: 37;

            suppose

             A13: not C1 is open;

            set g = ( modid ((X1 union X2),C1));

            set Y = ((X1 union X2) modified_with_respect_to C1);

            (g | Y1) = (g | X1) by Def5;

            then

             A14: (g | X1) is continuous Function of X1, Y by Th100;

            (g | Y2) = (g | X2) by Def5;

            then

             A15: (g | X2) is continuous Function of X2, Y by A5, Th99;

             not g is continuous Function of (X1 union X2), Y by A13, Th101;

            hence contradiction by A6, A14, A15;

          end;

            suppose

             A16: not C2 is open;

            set g = ( modid ((X1 union X2),C2));

            set Y = ((X1 union X2) modified_with_respect_to C2);

            (g | Y2) = (g | X2) by Def5;

            then

             A17: (g | X2) is continuous Function of X2, Y by Th100;

            (g | Y1) = (g | X1) by Def5;

            then

             A18: (g | X1) is continuous Function of X1, Y by A5, Th99;

             not g is continuous Function of (X1 union X2), Y by A16, Th101;

            hence contradiction by A6, A18, A17;

          end;

        end;

        hence contradiction;

      end;

    end;

    theorem :: TMAP_1:124

    

     Th124: (X1,X2) are_separated iff X1 misses X2 & for Y be non empty TopSpace, f be Function of X, Y st (f | X1) is continuous Function of X1, Y & (f | X2) is continuous Function of X2, Y holds (f | (X1 union X2)) is continuous Function of (X1 union X2), Y

    proof

      thus (X1,X2) are_separated implies X1 misses X2 & for Y be non empty TopSpace, f be Function of X, Y st (f | X1) is continuous Function of X1, Y & (f | X2) is continuous Function of X2, Y holds (f | (X1 union X2)) is continuous Function of (X1 union X2), Y

      proof

        assume

         A1: (X1,X2) are_separated ;

        hence X1 misses X2 by TSEP_1: 63;

        (X1,X2) are_weakly_separated by A1, TSEP_1: 78;

        hence thesis by Th117;

      end;

      thus X1 misses X2 & (for Y be non empty TopSpace, f be Function of X, Y st (f | X1) is continuous Function of X1, Y & (f | X2) is continuous Function of X2, Y holds (f | (X1 union X2)) is continuous Function of (X1 union X2), Y) implies (X1,X2) are_separated

      proof

        assume

         A2: X1 misses X2;

        assume

         A3: for Y be non empty TopSpace, f be Function of X, Y st (f | X1) is continuous Function of X1, Y & (f | X2) is continuous Function of X2, Y holds (f | (X1 union X2)) is continuous Function of (X1 union X2), Y;

        for Y be non empty TopSpace, g be Function of (X1 union X2), Y st (g | X1) is continuous Function of X1, Y & (g | X2) is continuous Function of X2, Y holds g is continuous Function of (X1 union X2), Y

        proof

          let Y be non empty TopSpace, g be Function of (X1 union X2), Y such that

           A4: (g | X1) is continuous Function of X1, Y and

           A5: (g | X2) is continuous Function of X2, Y;

          consider h be Function of X, Y such that

           A6: (h | (X1 union X2)) = g by Th57;

          X2 is SubSpace of (X1 union X2) by TSEP_1: 22;

          then

           A7: (h | X2) is continuous Function of X2, Y by A5, A6, Th70;

          X1 is SubSpace of (X1 union X2) by TSEP_1: 22;

          then (h | X1) is continuous Function of X1, Y by A4, A6, Th70;

          hence thesis by A3, A6, A7;

        end;

        hence thesis by A2, Th123;

      end;

    end;

    theorem :: TMAP_1:125

    for X1,X2 be non empty SubSpace of X st X = (X1 union X2) holds (X1,X2) are_separated iff X1 misses X2 & for Y be non empty TopSpace, f be Function of X, Y st (f | X1) is continuous Function of X1, Y & (f | X2) is continuous Function of X2, Y holds f is continuous Function of X, Y

    proof

      let X1,X2 be non empty SubSpace of X such that

       A1: X = (X1 union X2);

      thus (X1,X2) are_separated implies X1 misses X2 & for Y be non empty TopSpace, f be Function of X, Y st (f | X1) is continuous Function of X1, Y & (f | X2) is continuous Function of X2, Y holds f is continuous Function of X, Y

      proof

        assume

         A2: (X1,X2) are_separated ;

        hence X1 misses X2 by TSEP_1: 63;

        (X1,X2) are_weakly_separated by A2, TSEP_1: 78;

        hence thesis by A1, Th120;

      end;

      thus X1 misses X2 & (for Y be non empty TopSpace, f be Function of X, Y st (f | X1) is continuous Function of X1, Y & (f | X2) is continuous Function of X2, Y holds f is continuous Function of X, Y) implies (X1,X2) are_separated

      proof

        assume

         A3: X1 misses X2;

        assume

         A4: for Y be non empty TopSpace, f be Function of X, Y st (f | X1) is continuous Function of X1, Y & (f | X2) is continuous Function of X2, Y holds f is continuous Function of X, Y;

        for Y be non empty TopSpace, f be Function of X, Y st (f | X1) is continuous Function of X1, Y & (f | X2) is continuous Function of X2, Y holds (f | (X1 union X2)) is continuous Function of (X1 union X2), Y

        proof

          let Y be non empty TopSpace, f be Function of X, Y;

          assume (f | X1) is continuous Function of X1, Y & (f | X2) is continuous Function of X2, Y;

          then f is continuous Function of X, Y by A4;

          hence thesis;

        end;

        hence thesis by A3, Th124;

      end;

    end;

    begin

    definition

      let X,Y be non empty TopSpace, X1,X2 be non empty SubSpace of X;

      let f1 be Function of X1, Y, f2 be Function of X2, Y;

      assume

       A1: X1 misses X2 or (f1 | (X1 meet X2)) = (f2 | (X1 meet X2));

      :: TMAP_1:def12

      func f1 union f2 -> Function of (X1 union X2), Y means

      : Def12: (it | X1) = f1 & (it | X2) = f2;

      existence

      proof

        set B = the carrier of Y;

        set A = the carrier of (X1 union X2);

        set A2 = the carrier of X2;

        set A1 = the carrier of X1;

        

         A2: X1 is SubSpace of (X1 union X2) & X2 is SubSpace of (X1 union X2) by TSEP_1: 22;

        

         A3: A = (A1 \/ A2) by TSEP_1:def 2;

        

         A4: A1 meets A2 implies (f1 | (A1 /\ A2)) = (f2 | (A1 /\ A2))

        proof

          assume

           A5: A1 meets A2;

          then

           A6: X1 meets X2 by TSEP_1:def 3;

          then

           A7: (X1 meet X2) is SubSpace of X1 by TSEP_1: 27;

          

           A8: (X1 meet X2) is SubSpace of X2 by A6, TSEP_1: 27;

          

          thus (f1 | (A1 /\ A2)) = (f1 | the carrier of (X1 meet X2)) by A6, TSEP_1:def 4

          .= (f2 | (X1 meet X2)) by A1, A5, A7, Def5, TSEP_1:def 3

          .= (f2 | the carrier of (X1 meet X2)) by A8, Def5

          .= (f2 | (A1 /\ A2)) by A6, TSEP_1:def 4;

        end;

        reconsider A1, A2 as non empty Subset of A by A3, XBOOLE_1: 7;

        reconsider g1 = f1 as Function of A1, B;

        reconsider g2 = f2 as Function of A2, B;

        set G = (g1 union g2);

        the carrier of (X1 union X2) = (the carrier of X1 \/ the carrier of X2) by TSEP_1:def 2;

        then

        reconsider F = G as Function of (X1 union X2), Y;

        take F;

        (G | A1) = f1 & (G | A2) = f2 by A4, Def1, Th1;

        hence thesis by A2, Def5;

      end;

      uniqueness

      proof

        set A = the carrier of (X1 union X2);

        

         A9: X2 is SubSpace of (X1 union X2) by TSEP_1: 22;

        set A2 = the carrier of X2;

        

         A10: X1 is SubSpace of (X1 union X2) by TSEP_1: 22;

        set A1 = the carrier of X1;

        let F be Function of (X1 union X2), Y, G be Function of (X1 union X2), Y such that

         A11: (F | X1) = f1 and

         A12: (F | X2) = f2 and

         A13: (G | X1) = f1 and

         A14: (G | X2) = f2;

        

         A15: A = (A1 \/ A2) by TSEP_1:def 2;

        now

          let a be Element of A;

           A16:

          now

            assume

             A17: a in A2;

            

            hence (F . a) = ((F | A2) . a) by FUNCT_1: 49

            .= (f2 . a) by A12, A9, Def5

            .= ((G | A2) . a) by A14, A9, Def5

            .= (G . a) by A17, FUNCT_1: 49;

          end;

          now

            assume

             A18: a in A1;

            

            hence (F . a) = ((F | A1) . a) by FUNCT_1: 49

            .= (f1 . a) by A11, A10, Def5

            .= ((G | A1) . a) by A13, A10, Def5

            .= (G . a) by A18, FUNCT_1: 49;

          end;

          hence (F . a) = (G . a) by A15, A16, XBOOLE_0:def 3;

        end;

        hence thesis by FUNCT_2: 63;

      end;

    end

    reserve X,Y for non empty TopSpace;

    theorem :: TMAP_1:126

    

     Th126: for X1,X2 be non empty SubSpace of X holds for g be Function of (X1 union X2), Y holds g = ((g | X1) union (g | X2))

    proof

      let X1,X2 be non empty SubSpace of X;

      let g be Function of (X1 union X2), Y;

      now

        assume

         A1: X1 meets X2;

        then

         A2: (X1 meet X2) is SubSpace of X2 by TSEP_1: 27;

        

         A3: X2 is SubSpace of (X1 union X2) by TSEP_1: 22;

        

         A4: X1 is SubSpace of (X1 union X2) by TSEP_1: 22;

        (X1 meet X2) is SubSpace of X1 by A1, TSEP_1: 27;

        

        hence ((g | X1) | (X1 meet X2)) = (g | (X1 meet X2)) by A4, Th72

        .= ((g | X2) | (X1 meet X2)) by A2, A3, Th72;

      end;

      hence thesis by Def12;

    end;

    theorem :: TMAP_1:127

    for X1,X2 be non empty SubSpace of X st X = (X1 union X2) holds for g be Function of X, Y holds g = ((g | X1) union (g | X2))

    proof

      let X1,X2 be non empty SubSpace of X such that

       A1: X = (X1 union X2);

      let g be Function of X, Y;

      reconsider h = g as Function of (X1 union X2), Y by A1;

      X2 is SubSpace of (X1 union X2) by TSEP_1: 22;

      then

       A2: (h | X2) = (g | X2) by Def5;

      X1 is SubSpace of (X1 union X2) by TSEP_1: 22;

      then (h | X1) = (g | X1) by Def5;

      hence thesis by A2, Th126;

    end;

    theorem :: TMAP_1:128

    

     Th128: for X1,X2 be non empty SubSpace of X st X1 meets X2 holds for f1 be Function of X1, Y, f2 be Function of X2, Y holds ((f1 union f2) | X1) = f1 & ((f1 union f2) | X2) = f2 iff (f1 | (X1 meet X2)) = (f2 | (X1 meet X2))

    proof

      let X1,X2 be non empty SubSpace of X such that

       A1: X1 meets X2;

      let f1 be Function of X1, Y, f2 be Function of X2, Y;

      thus ((f1 union f2) | X1) = f1 & ((f1 union f2) | X2) = f2 implies (f1 | (X1 meet X2)) = (f2 | (X1 meet X2))

      proof

        

         A2: (X1 meet X2) is SubSpace of X2 & X2 is SubSpace of (X1 union X2) by A1, TSEP_1: 22, TSEP_1: 27;

        assume that

         A3: ((f1 union f2) | X1) = f1 and

         A4: ((f1 union f2) | X2) = f2;

        (X1 meet X2) is SubSpace of X1 & X1 is SubSpace of (X1 union X2) by A1, TSEP_1: 22, TSEP_1: 27;

        then ((f1 union f2) | (X1 meet X2)) = (f1 | (X1 meet X2)) by A3, Th72;

        hence thesis by A2, A4, Th72;

      end;

      thus thesis by Def12;

    end;

    theorem :: TMAP_1:129

    for X1,X2 be non empty SubSpace of X, f1 be Function of X1, Y, f2 be Function of X2, Y st (f1 | (X1 meet X2)) = (f2 | (X1 meet X2)) holds (X1 is SubSpace of X2 iff (f1 union f2) = f2) & (X2 is SubSpace of X1 iff (f1 union f2) = f1)

    proof

      let X1,X2 be non empty SubSpace of X, f1 be Function of X1, Y, f2 be Function of X2, Y;

      reconsider Y1 = X1, Y2 = X2, Y3 = (X1 union X2) as SubSpace of (X1 union X2) by TSEP_1: 2, TSEP_1: 22;

      assume

       A1: (f1 | (X1 meet X2)) = (f2 | (X1 meet X2));

       A2:

      now

        assume X1 is SubSpace of X2;

        then

         A3: the TopStruct of X2 = (X1 union X2) by TSEP_1: 23;

        ((f1 union f2) | X2) = f2 by A1, Def12;

        then ((f1 union f2) | the carrier of Y2) = f2 by Def5;

        then ((f1 union f2) | the carrier of Y3) = f2 by A3;

        then ((f1 union f2) | (X1 union X2)) = f2 by Def5;

        hence (f1 union f2) = f2 by Th67;

      end;

       A4:

      now

        assume X2 is SubSpace of X1;

        then

         A5: the TopStruct of X1 = (X1 union X2) by TSEP_1: 23;

        ((f1 union f2) | X1) = f1 by A1, Def12;

        then ((f1 union f2) | the carrier of Y1) = f1 by Def5;

        then ((f1 union f2) | the carrier of Y3) = f1 by A5;

        then ((f1 union f2) | (X1 union X2)) = f1 by Def5;

        hence (f1 union f2) = f1 by Th67;

      end;

      now

        

         A6: ( dom (f1 union f2)) = the carrier of (X1 union X2) & ( dom f2) = the carrier of X2 by FUNCT_2:def 1;

        assume (f1 union f2) = f2;

        then (X1 union X2) = the TopStruct of X2 by A6, TSEP_1: 5;

        hence X1 is SubSpace of X2 by TSEP_1: 23;

      end;

      hence X1 is SubSpace of X2 iff (f1 union f2) = f2 by A2;

      now

        

         A7: ( dom (f1 union f2)) = the carrier of (X1 union X2) & ( dom f1) = the carrier of X1 by FUNCT_2:def 1;

        assume (f1 union f2) = f1;

        then (X1 union X2) = the TopStruct of X1 by A7, TSEP_1: 5;

        hence X2 is SubSpace of X1 by TSEP_1: 23;

      end;

      hence X2 is SubSpace of X1 iff (f1 union f2) = f1 by A4;

    end;

    theorem :: TMAP_1:130

    for X1,X2 be non empty SubSpace of X, f1 be Function of X1, Y, f2 be Function of X2, Y st X1 misses X2 or (f1 | (X1 meet X2)) = (f2 | (X1 meet X2)) holds (f1 union f2) = (f2 union f1)

    proof

      let X1,X2 be non empty SubSpace of X, f1 be Function of X1, Y, f2 be Function of X2, Y;

      assume X1 misses X2 or (f1 | (X1 meet X2)) = (f2 | (X1 meet X2));

      then ((f1 union f2) | X1) = f1 & ((f1 union f2) | X2) = f2 by Def12;

      hence thesis by Th126;

    end;

    theorem :: TMAP_1:131

    for X1,X2,X3 be non empty SubSpace of X, f1 be Function of X1, Y, f2 be Function of X2, Y, f3 be Function of X3, Y st (X1 misses X2 or (f1 | (X1 meet X2)) = (f2 | (X1 meet X2))) & (X1 misses X3 or (f1 | (X1 meet X3)) = (f3 | (X1 meet X3))) & (X2 misses X3 or (f2 | (X2 meet X3)) = (f3 | (X2 meet X3))) holds ((f1 union f2) union f3) = (f1 union (f2 union f3))

    proof

      let X1,X2,X3 be non empty SubSpace of X, f1 be Function of X1, Y, f2 be Function of X2, Y, f3 be Function of X3, Y such that

       A1: X1 misses X2 or (f1 | (X1 meet X2)) = (f2 | (X1 meet X2)) and

       A2: X1 misses X3 or (f1 | (X1 meet X3)) = (f3 | (X1 meet X3)) and

       A3: X2 misses X3 or (f2 | (X2 meet X3)) = (f3 | (X2 meet X3));

      set g = ((f1 union f2) union f3);

      

       A4: ((X1 union X2) union X3) = (X1 union (X2 union X3)) by TSEP_1: 21;

      then

      reconsider f = g as Function of (X1 union (X2 union X3)), Y;

      

       A5: (X1 union X2) is SubSpace of (X1 union (X2 union X3)) by A4, TSEP_1: 22;

       A6:

      now

        assume

         A7: (X1 union X2) meets X3;

        now

          per cases by A7, Th34;

            suppose

             A8: X1 meets X3 & not X2 meets X3;

            then

             A9: ((X1 union X2) meet X3) = (X1 meet X3) by Th26;

            

             A10: X1 is SubSpace of (X1 union X2) by TSEP_1: 22;

            (X1 meet X3) is SubSpace of X1 by A8, TSEP_1: 27;

            

            then ((f1 union f2) | (X1 meet X3)) = (((f1 union f2) | X1) | (X1 meet X3)) by A10, Th72

            .= (f1 | (X1 meet X3)) by A1, Def12;

            hence ((f1 union f2) | ((X1 union X2) meet X3)) = (f3 | ((X1 union X2) meet X3)) by A2, A8, A9;

          end;

            suppose

             A11: not X1 meets X3 & X2 meets X3;

            then

             A12: ((X1 union X2) meet X3) = (X2 meet X3) by Th26;

            

             A13: X2 is SubSpace of (X1 union X2) by TSEP_1: 22;

            (X2 meet X3) is SubSpace of X2 by A11, TSEP_1: 27;

            

            then ((f1 union f2) | (X2 meet X3)) = (((f1 union f2) | X2) | (X2 meet X3)) by A13, Th72

            .= (f2 | (X2 meet X3)) by A1, Def12;

            hence ((f1 union f2) | ((X1 union X2) meet X3)) = (f3 | ((X1 union X2) meet X3)) by A3, A11, A12;

          end;

            suppose

             A14: X1 meets X3 & X2 meets X3;

            then (X1 meet X3) is SubSpace of X3 & (X2 meet X3) is SubSpace of X3 by TSEP_1: 27;

            then

             A15: ((X1 meet X3) union (X2 meet X3)) is SubSpace of X3 by Th24;

            

             A16: (X2 meet X3) is SubSpace of X2 by A14, TSEP_1: 27;

            

             A17: (X1 meet X3) is SubSpace of ((X1 meet X3) union (X2 meet X3)) by TSEP_1: 22;

            then

             A18: ((f3 | ((X1 meet X3) union (X2 meet X3))) | (X1 meet X3)) = (f3 | (X1 meet X3)) by A15, Th72;

            

             A19: (X1 meet X3) is SubSpace of X1 by A14, TSEP_1: 27;

            then

             A20: ((X1 meet X3) union (X2 meet X3)) is SubSpace of (X1 union X2) by A16, Th22;

            then

             A21: (((f1 union f2) | ((X1 meet X3) union (X2 meet X3))) | (X1 meet X3)) = ((f1 union f2) | (X1 meet X3)) by A17, Th72;

            X2 is SubSpace of (X1 union X2) by TSEP_1: 22;

            

            then

             A22: ((f1 union f2) | (X2 meet X3)) = (((f1 union f2) | X2) | (X2 meet X3)) by A16, Th72

            .= (f2 | (X2 meet X3)) by A1, Def12;

            set v = (f3 | ((X1 meet X3) union (X2 meet X3)));

            

             A23: (X2 meet X3) is SubSpace of ((X1 meet X3) union (X2 meet X3)) by TSEP_1: 22;

            then

             A24: ((f3 | ((X1 meet X3) union (X2 meet X3))) | (X2 meet X3)) = (f3 | (X2 meet X3)) by A15, Th72;

            X1 is SubSpace of (X1 union X2) by TSEP_1: 22;

            

            then

             A25: ((f1 union f2) | (X1 meet X3)) = (((f1 union f2) | X1) | (X1 meet X3)) by A19, Th72

            .= (f1 | (X1 meet X3)) by A1, Def12;

            

             A26: (((f1 union f2) | ((X1 meet X3) union (X2 meet X3))) | (X2 meet X3)) = ((f1 union f2) | (X2 meet X3)) by A20, A23, Th72;

            ((f1 union f2) | ((X1 union X2) meet X3)) = ((f1 union f2) | ((X1 meet X3) union (X2 meet X3))) by A14, TSEP_1: 32

            .= ((v | (X1 meet X3)) union (v | (X2 meet X3))) by A2, A3, A14, A25, A22, A21, A26, A18, A24, Th126

            .= v by Th126;

            hence ((f1 union f2) | ((X1 union X2) meet X3)) = (f3 | ((X1 union X2) meet X3)) by A14, TSEP_1: 32;

          end;

        end;

        hence ((f1 union f2) | ((X1 union X2) meet X3)) = (f3 | ((X1 union X2) meet X3));

      end;

      then (X1 union X2) is SubSpace of ((X1 union X2) union X3) & (g | (X1 union X2)) = (f1 union f2) by Def12, TSEP_1: 22;

      then

       A27: (f | the carrier of (X1 union X2)) = (f1 union f2) by Def5;

      

       A28: X3 is SubSpace of (X1 union (X2 union X3)) by A4, TSEP_1: 22;

      

       A29: (X2 union X3) is SubSpace of (X1 union (X2 union X3)) by TSEP_1: 22;

      X3 is SubSpace of ((X1 union X2) union X3) & (g | X3) = f3 by A6, Def12, TSEP_1: 22;

      then

       A30: (f | the carrier of X3) = f3 by Def5;

      

       A31: (X1 union X2) is SubSpace of (X1 union (X2 union X3)) by A4, TSEP_1: 22;

      X3 is SubSpace of (X2 union X3) by TSEP_1: 22;

      

      then

       A32: ((f | (X2 union X3)) | X3) = (f | X3) by A29, Th72

      .= f3 by A28, A30, Def5;

      X2 is SubSpace of (X1 union X2) by TSEP_1: 22;

      

      then

       A33: (f | X2) = ((f | (X1 union X2)) | X2) by A31, Th72

      .= ((f1 union f2) | X2) by A5, A27, Def5;

      X2 is SubSpace of (X2 union X3) by TSEP_1: 22;

      

      then ((f | (X2 union X3)) | X2) = (f | X2) by A29, Th72

      .= f2 by A1, A33, Def12;

      then

       A34: (f | (X2 union X3)) = (f2 union f3) by A32, Th126;

      X1 is SubSpace of (X1 union X2) by TSEP_1: 22;

      

      then (f | X1) = ((f | (X1 union X2)) | X1) by A31, Th72

      .= ((f1 union f2) | X1) by A5, A27, Def5;

      then (f | X1) = f1 by A1, Def12;

      hence thesis by A34, Th126;

    end;

    theorem :: TMAP_1:132

    for X1,X2 be non empty SubSpace of X st X1 meets X2 holds for f1 be continuous Function of X1, Y, f2 be continuous Function of X2, Y st (f1 | (X1 meet X2)) = (f2 | (X1 meet X2)) holds (X1,X2) are_weakly_separated implies (f1 union f2) is continuous Function of (X1 union X2), Y

    proof

      let X1,X2 be non empty SubSpace of X such that

       A1: X1 meets X2;

      let f1 be continuous Function of X1, Y, f2 be continuous Function of X2, Y;

      assume (f1 | (X1 meet X2)) = (f2 | (X1 meet X2));

      then

       A2: ((f1 union f2) | X1) = f1 & ((f1 union f2) | X2) = f2 by A1, Th128;

      assume (X1,X2) are_weakly_separated ;

      hence thesis by A2, Th114;

    end;

    theorem :: TMAP_1:133

    

     Th133: for X1,X2 be non empty SubSpace of X st X1 misses X2 holds for f1 be continuous Function of X1, Y, f2 be continuous Function of X2, Y holds (X1,X2) are_weakly_separated implies (f1 union f2) is continuous Function of (X1 union X2), Y

    proof

      let X1,X2 be non empty SubSpace of X such that

       A1: X1 misses X2;

      let f1 be continuous Function of X1, Y, f2 be continuous Function of X2, Y;

      assume

       A2: (X1,X2) are_weakly_separated ;

      ((f1 union f2) | X1) = f1 & ((f1 union f2) | X2) = f2 by A1, Def12;

      hence thesis by A2, Th114;

    end;

    theorem :: TMAP_1:134

    for X1,X2 be closed non empty SubSpace of X st X1 meets X2 holds for f1 be continuous Function of X1, Y, f2 be continuous Function of X2, Y st (f1 | (X1 meet X2)) = (f2 | (X1 meet X2)) holds (f1 union f2) is continuous Function of (X1 union X2), Y

    proof

      let X1,X2 be closed non empty SubSpace of X such that

       A1: X1 meets X2;

      let f1 be continuous Function of X1, Y, f2 be continuous Function of X2, Y;

      assume (f1 | (X1 meet X2)) = (f2 | (X1 meet X2));

      then ((f1 union f2) | X1) = f1 & ((f1 union f2) | X2) = f2 by A1, Th128;

      hence thesis by Th115;

    end;

    theorem :: TMAP_1:135

    for X1,X2 be open non empty SubSpace of X st X1 meets X2 holds for f1 be continuous Function of X1, Y, f2 be continuous Function of X2, Y st (f1 | (X1 meet X2)) = (f2 | (X1 meet X2)) holds (f1 union f2) is continuous Function of (X1 union X2), Y

    proof

      let X1,X2 be open non empty SubSpace of X such that

       A1: X1 meets X2;

      let f1 be continuous Function of X1, Y, f2 be continuous Function of X2, Y;

      assume (f1 | (X1 meet X2)) = (f2 | (X1 meet X2));

      then ((f1 union f2) | X1) = f1 & ((f1 union f2) | X2) = f2 by A1, Th128;

      hence thesis by Th116;

    end;

    theorem :: TMAP_1:136

    for X1,X2 be closed non empty SubSpace of X st X1 misses X2 holds for f1 be continuous Function of X1, Y, f2 be continuous Function of X2, Y holds (f1 union f2) is continuous Function of (X1 union X2), Y

    proof

      let X1,X2 be closed non empty SubSpace of X such that

       A1: X1 misses X2;

      let f1 be continuous Function of X1, Y, f2 be continuous Function of X2, Y;

      ((f1 union f2) | X1) = f1 & ((f1 union f2) | X2) = f2 by A1, Def12;

      hence thesis by Th115;

    end;

    theorem :: TMAP_1:137

    for X1,X2 be open non empty SubSpace of X st X1 misses X2 holds for f1 be continuous Function of X1, Y, f2 be continuous Function of X2, Y holds (f1 union f2) is continuous Function of (X1 union X2), Y

    proof

      let X1,X2 be open non empty SubSpace of X such that

       A1: X1 misses X2;

      let f1 be continuous Function of X1, Y, f2 be continuous Function of X2, Y;

      ((f1 union f2) | X1) = f1 & ((f1 union f2) | X2) = f2 by A1, Def12;

      hence thesis by Th116;

    end;

    theorem :: TMAP_1:138

    for X1,X2 be non empty SubSpace of X holds (X1,X2) are_separated iff X1 misses X2 & for Y be non empty TopSpace, f1 be continuous Function of X1, Y, f2 be continuous Function of X2, Y holds (f1 union f2) is continuous Function of (X1 union X2), Y

    proof

      let X1,X2 be non empty SubSpace of X;

      thus (X1,X2) are_separated implies X1 misses X2 & for Y be non empty TopSpace, f1 be continuous Function of X1, Y, f2 be continuous Function of X2, Y holds (f1 union f2) is continuous Function of (X1 union X2), Y

      proof

        assume

         A1: (X1,X2) are_separated ;

        hence X1 misses X2 by TSEP_1: 63;

        (X1,X2) are_weakly_separated by A1, TSEP_1: 78;

        hence thesis by A1, Th133, TSEP_1: 63;

      end;

      thus X1 misses X2 & (for Y be non empty TopSpace, f1 be continuous Function of X1, Y, f2 be continuous Function of X2, Y holds (f1 union f2) is continuous Function of (X1 union X2), Y) implies (X1,X2) are_separated

      proof

        assume

         A2: X1 misses X2;

        assume

         A3: for Y be non empty TopSpace, f1 be continuous Function of X1, Y, f2 be continuous Function of X2, Y holds (f1 union f2) is continuous Function of (X1 union X2), Y;

        now

          let Y be non empty TopSpace, g be Function of (X1 union X2), Y;

          assume that

           A4: (g | X1) is continuous Function of X1, Y and

           A5: (g | X2) is continuous Function of X2, Y;

          reconsider f2 = (g | X2) as continuous Function of X2, Y by A5;

          reconsider f1 = (g | X1) as continuous Function of X1, Y by A4;

          g = (f1 union f2) by Th126;

          hence g is continuous Function of (X1 union X2), Y by A3;

        end;

        hence thesis by A2, Th123;

      end;

    end;

    theorem :: TMAP_1:139

    for X1,X2 be non empty SubSpace of X st X = (X1 union X2) holds for f1 be continuous Function of X1, Y, f2 be continuous Function of X2, Y st ((f1 union f2) | X1) = f1 & ((f1 union f2) | X2) = f2 holds (X1,X2) are_weakly_separated implies (f1 union f2) is continuous Function of X, Y

    proof

      let X1,X2 be non empty SubSpace of X such that

       A1: X = (X1 union X2);

      let f1 be continuous Function of X1, Y, f2 be continuous Function of X2, Y such that

       A2: ((f1 union f2) | X1) = f1 & ((f1 union f2) | X2) = f2;

      reconsider g = (f1 union f2) as Function of X, Y by A1;

      assume

       A3: (X1,X2) are_weakly_separated ;

      (g | X1) = f1 & (g | X2) = f2 by A1, A2, Def5;

      hence thesis by A1, A3, Th120;

    end;

    theorem :: TMAP_1:140

    for X1,X2 be closed non empty SubSpace of X, f1 be continuous Function of X1, Y, f2 be continuous Function of X2, Y st X = (X1 union X2) & ((f1 union f2) | X1) = f1 & ((f1 union f2) | X2) = f2 holds (f1 union f2) is continuous Function of X, Y

    proof

      let X1,X2 be closed non empty SubSpace of X, f1 be continuous Function of X1, Y, f2 be continuous Function of X2, Y such that

       A1: X = (X1 union X2) and

       A2: ((f1 union f2) | X1) = f1 & ((f1 union f2) | X2) = f2;

      reconsider g = (f1 union f2) as Function of X, Y by A1;

      (g | X1) = f1 & (g | X2) = f2 by A1, A2, Def5;

      hence thesis by A1, Th121;

    end;

    theorem :: TMAP_1:141

    for X1,X2 be open non empty SubSpace of X, f1 be continuous Function of X1, Y, f2 be continuous Function of X2, Y st X = (X1 union X2) & ((f1 union f2) | X1) = f1 & ((f1 union f2) | X2) = f2 holds (f1 union f2) is continuous Function of X, Y

    proof

      let X1,X2 be open non empty SubSpace of X, f1 be continuous Function of X1, Y, f2 be continuous Function of X2, Y such that

       A1: X = (X1 union X2) and

       A2: ((f1 union f2) | X1) = f1 & ((f1 union f2) | X2) = f2;

      reconsider g = (f1 union f2) as Function of X, Y by A1;

      (g | X1) = f1 & (g | X2) = f2 by A1, A2, Def5;

      hence thesis by A1, Th122;

    end;

    theorem :: TMAP_1:142

    for A,B be non empty set holds for A1,A2 be non empty Subset of A holds for f1 be Function of A1, B, f2 be Function of A2, B st (f1 | (A1 /\ A2)) = (f2 | (A1 /\ A2)) holds ((f1 union f2) | A1) = f1 & ((f1 union f2) | A2) = f2 by Def1;