t_0topsp.miz



    begin

    theorem :: T_0TOPSP:1

    

     Th1: for X,Y be non empty set, f be Function of X, Y holds for A be Subset of X st for x1,x2 be Element of X holds x1 in A & (f . x1) = (f . x2) implies x2 in A holds (f " (f .: A)) = A

    proof

      let X,Y be non empty set;

      let f be Function of X, Y;

      let A be Subset of X;

      assume

       A1: for x1,x2 be Element of X holds x1 in A & (f . x1) = (f . x2) implies x2 in A;

      for x be object st x in (f " (f .: A)) holds x in A

      proof

        let x be object;

        assume

         A2: x in (f " (f .: A));

        then (f . x) in (f .: A) by FUNCT_1:def 7;

        then ex x0 be object st x0 in X & x0 in A & (f . x) = (f . x0) by FUNCT_2: 64;

        hence thesis by A1, A2;

      end;

      then A c= (f " (f .: A)) & (f " (f .: A)) c= A by FUNCT_2: 42, TARSKI:def 3;

      hence thesis by XBOOLE_0:def 10;

    end;

    definition

      let T,S be TopStruct;

      :: T_0TOPSP:def1

      pred T,S are_homeomorphic means ex f be Function of T, S st f is being_homeomorphism;

    end

    definition

      let T,S be TopStruct;

      let f be Function of T, S;

      :: T_0TOPSP:def2

      attr f is open means for A be Subset of T st A is open holds (f .: A) is open;

      correctness ;

    end

    definition

      let T be non empty TopStruct;

      :: T_0TOPSP:def3

      func Indiscernibility (T) -> Equivalence_Relation of the carrier of T means

      : Def3: for p,q be Point of T holds [p, q] in it iff for A be Subset of T st A is open holds p in A iff q in A;

      existence

      proof

        defpred X[ set, set] means for A be Subset of T st A is open holds $1 in A iff $2 in A;

        consider R be Relation of the carrier of T, the carrier of T such that

         A1: for p,q be Element of T holds [p, q] in R iff X[p, q] from RELSET_1:sch 2;

        

         A2: R is_transitive_in the carrier of T

        proof

          let x,y,z be object;

          assume that

           A3: x in the carrier of T & y in the carrier of T & z in the carrier of T and

           A4: [x, y] in R and

           A5: [y, z] in R;

          reconsider x9 = x, y9 = y, z9 = z as Element of T by A3;

          for A be Subset of T st A is open holds x9 in A iff z9 in A

          proof

            let A be Subset of T;

            assume

             A6: A is open;

            then x9 in A iff y9 in A by A1, A4;

            hence thesis by A1, A5, A6;

          end;

          hence thesis by A1;

        end;

        R is_reflexive_in the carrier of T

        proof

          let x be object;

          

           A7: for A be Subset of T st A is open holds x in A iff x in A;

          assume x in the carrier of T;

          hence thesis by A1, A7;

        end;

        then

         A8: ( dom R) = the carrier of T & ( field R) = the carrier of T by ORDERS_1: 13;

        R is_symmetric_in the carrier of T

        proof

          let x,y be object;

          assume that

           A9: x in the carrier of T & y in the carrier of T and

           A10: [x, y] in R;

          for A be Subset of T st A is open holds y in A iff x in A by A1, A9, A10;

          hence thesis by A1, A9;

        end;

        then

        reconsider R as Equivalence_Relation of the carrier of T by A8, A2, PARTFUN1:def 2, RELAT_2:def 11, RELAT_2:def 16;

        take R;

        let p,q be Point of T;

        thus [p, q] in R implies for A be Subset of T st A is open holds p in A iff q in A by A1;

        assume for A be Subset of T st A is open holds p in A iff q in A;

        hence thesis by A1;

      end;

      uniqueness

      proof

        let R1,R2 be Equivalence_Relation of the carrier of T;

        assume that

         A11: for p,q be Point of T holds [p, q] in R1 iff for A be Subset of T st A is open holds p in A iff q in A and

         A12: for p,q be Point of T holds [p, q] in R2 iff for A be Subset of T st A is open holds p in A iff q in A;

        let x,y be Point of T;

         [x, y] in R1 iff for A be Subset of T st A is open holds x in A iff y in A by A11;

        hence thesis by A12;

      end;

    end

    definition

      let T be non empty TopStruct;

      :: T_0TOPSP:def4

      func Indiscernible (T) -> non empty a_partition of the carrier of T equals ( Class ( Indiscernibility T));

      coherence ;

    end

    definition

      let T be non empty TopSpace;

      :: T_0TOPSP:def5

      func T_0-reflex (T) -> TopSpace equals ( space ( Indiscernible T));

      correctness ;

    end

    registration

      let T be non empty TopSpace;

      cluster ( T_0-reflex T) -> non empty;

      coherence ;

    end

    definition

      let T be non empty TopSpace;

      :: T_0TOPSP:def6

      func T_0-canonical_map T -> continuous Function of T, ( T_0-reflex T) equals ( Proj ( Indiscernible T));

      coherence ;

    end

    theorem :: T_0TOPSP:2

    

     Th2: for T be non empty TopSpace, V be Subset of ( T_0-reflex T) holds V is open iff ( union V) in the topology of T

    proof

      let T be non empty TopSpace;

      let V be Subset of ( T_0-reflex T);

      

       A1: V is Subset of ( Indiscernible T) by BORSUK_1:def 7;

      thus V is open implies ( union V) in the topology of T by A1, BORSUK_1: 27;

      assume ( union V) in the topology of T;

      then V in the topology of ( space ( Indiscernible T)) by A1, BORSUK_1: 27;

      hence thesis;

    end;

    theorem :: T_0TOPSP:3

    

     Th3: for T be non empty TopSpace, C be set holds C is Point of ( T_0-reflex T) iff ex p be Point of T st C = ( Class (( Indiscernibility T),p))

    proof

      let T be non empty TopSpace;

      set TR = ( T_0-reflex T);

      set R = ( Indiscernibility T);

      let C be set;

      hereby

        assume C is Point of TR;

        then C in the carrier of TR;

        then C in ( Indiscernible T) by BORSUK_1:def 7;

        hence ex p be Point of T st C = ( Class (R,p)) by EQREL_1: 36;

      end;

      assume ex p be Point of T st C = ( Class (R,p));

      then C in ( Class R) by EQREL_1:def 3;

      hence thesis by BORSUK_1:def 7;

    end;

    theorem :: T_0TOPSP:4

    

     Th4: for T be non empty TopSpace, p be Point of T holds (( T_0-canonical_map T) . p) = ( Class (( Indiscernibility T),p))

    proof

      let T be non empty TopSpace;

      let p be Point of T;

      set F = ( T_0-canonical_map T);

      set R = ( Indiscernibility T);

      (F . p) in the carrier of ( T_0-reflex T);

      then (F . p) in ( Indiscernible T) by BORSUK_1:def 7;

      then

      consider y be Element of T such that

       A1: (F . p) = ( Class (R,y)) by EQREL_1: 36;

      p in ( Class (R,y)) by A1, BORSUK_1: 28;

      hence thesis by A1, EQREL_1: 23;

    end;

    theorem :: T_0TOPSP:5

    

     Th5: for T be non empty TopSpace, p,q be Point of T holds (( T_0-canonical_map T) . q) = (( T_0-canonical_map T) . p) iff [q, p] in ( Indiscernibility T)

    proof

      let T be non empty TopSpace;

      let p,q be Point of T;

      set F = ( T_0-canonical_map T);

      set R = ( Indiscernibility T);

      hereby

        assume (F . q) = (F . p);

        then q in (F . p) by BORSUK_1: 28;

        then q in ( Class (R,p)) by Th4;

        hence [q, p] in R by EQREL_1: 19;

      end;

      assume [q, p] in R;

      then ( Class (R,q)) = ( Class (R,p)) by EQREL_1: 35;

      then (F . q) = ( Class (R,p)) by Th4;

      hence thesis by Th4;

    end;

    theorem :: T_0TOPSP:6

    

     Th6: for T be non empty TopSpace, A be Subset of T st A is open holds for p,q be Point of T holds p in A & (( T_0-canonical_map T) . p) = (( T_0-canonical_map T) . q) implies q in A

    proof

      let T be non empty TopSpace;

      let A be Subset of T such that

       A1: A is open;

      set F = ( T_0-canonical_map T);

      let p,q be Point of T;

      assume that

       A2: p in A and

       A3: (F . p) = (F . q);

      

       A4: (F . p) = ( Class (( Indiscernibility T),p)) by Th4;

      q in (F . p) by A3, BORSUK_1: 28;

      then [q, p] in ( Indiscernibility T) by A4, EQREL_1: 19;

      hence thesis by A1, A2, Def3;

    end;

    theorem :: T_0TOPSP:7

    

     Th7: for T be non empty TopSpace, A be Subset of T st A is open holds for C be Subset of T st C in ( Indiscernible T) & C meets A holds C c= A

    proof

      let T be non empty TopSpace;

      let A be Subset of T such that

       A1: A is open;

      set R = ( Indiscernibility T);

      let C be Subset of T;

      assume that

       A2: C in ( Indiscernible T) and

       A3: C meets A;

      consider y be object such that

       A4: y in C and

       A5: y in A by A3, XBOOLE_0: 3;

      consider x be object such that x in the carrier of T and

       A6: C = ( Class (R,x)) by A2, EQREL_1:def 3;

      for p be object st p in C holds p in A

      proof

        let p be object;

         [y, x] in R by A6, A4, EQREL_1: 19;

        then

         A7: [x, y] in R by EQREL_1: 6;

        assume

         A8: p in C;

        then [p, x] in R by A6, EQREL_1: 19;

        then [p, y] in R by A7, EQREL_1: 7;

        hence thesis by A1, A5, A8, Def3;

      end;

      hence thesis by TARSKI:def 3;

    end;

    theorem :: T_0TOPSP:8

    

     Th8: for T be non empty TopSpace holds ( T_0-canonical_map T) is open

    proof

      let T be non empty TopSpace;

      set F = ( T_0-canonical_map T);

      for A be Subset of T st A is open holds (F .: A) is open

      proof

        set D = ( Indiscernible T);

        

         A1: F = ( proj D) by BORSUK_1:def 8;

        let A be Subset of T such that

         A2: A is open;

        

         A3: for C be Subset of T st C in D & C meets A holds C c= A by A2, Th7;

        set A9 = (F .: A);

        A9 is Subset of D by BORSUK_1:def 7;

        then (F " A9) = ( union A9) by A1, EQREL_1: 67;

        then A = ( union A9) by A1, A3, EQREL_1: 69;

        then ( union A9) in the topology of T by A2;

        hence thesis by Th2;

      end;

      hence thesis;

    end;

    

     Lm1: for T be non empty TopSpace, x,y be Point of ( T_0-reflex T) st x <> y holds ex V be Subset of ( T_0-reflex T) st V is open & (x in V & not y in V or y in V & not x in V)

    proof

      let T be non empty TopSpace;

      set S = ( T_0-reflex T);

      set F = ( T_0-canonical_map T);

      assume not (for x,y be Point of S st not x = y holds ex V be Subset of S st V is open & (x in V & not y in V or y in V & not x in V));

      then

      consider x,y be Point of S such that

       A1: x <> y and

       A2: for V be Subset of S st V is open holds x in V iff y in V;

      reconsider x, y as Point of ( space ( Indiscernible T));

      consider p be Point of T such that

       A3: (F . p) = x by BORSUK_1: 29;

      consider q be Point of T such that

       A4: (F . q) = y by BORSUK_1: 29;

      for A be Subset of T st A is open holds p in A iff q in A

      proof

        let A be Subset of T such that

         A5: A is open;

        F is open by Th8;

        then

         A6: (F .: A) is open by A5;

        reconsider F as Function of the carrier of T, the carrier of S;

        hereby

          assume p in A;

          then x in (F .: A) by A3, FUNCT_2: 35;

          then (F . q) in (F .: A) by A2, A4, A6;

          then ex x be object st x in the carrier of T & x in A & (F . q) = (F . x) by FUNCT_2: 64;

          hence q in A by A5, Th6;

        end;

        assume q in A;

        then y in (F .: A) by A4, FUNCT_2: 35;

        then (F . p) in (F .: A) by A2, A3, A6;

        then ex x be object st x in the carrier of T & x in A & (F . p) = (F . x) by FUNCT_2: 64;

        hence thesis by A5, Th6;

      end;

      then [p, q] in ( Indiscernibility T) by Def3;

      hence contradiction by A1, A3, A4, Th5;

    end;

    definition

      let T be TopStruct;

      :: original: T_0

      redefine

      :: T_0TOPSP:def7

      attr T is T_0 means

      : Def7: T is empty or for x,y be Point of T st x <> y holds ex V be Subset of T st V is open & (x in V & not y in V or y in V & not x in V);

      compatibility ;

    end

    registration

      cluster T_0 non empty for TopSpace;

      existence

      proof

        set T = the non empty TopSpace;

        take ( T_0-reflex T);

        for x,y be Point of ( T_0-reflex T) st x <> y holds ex V be Subset of ( T_0-reflex T) st V is open & (x in V & not y in V or y in V & not x in V) by Lm1;

        hence thesis;

      end;

    end

    definition

      mode T_0-TopSpace is T_0 non empty TopSpace;

    end

    theorem :: T_0TOPSP:9

    for T be non empty TopSpace holds ( T_0-reflex T) is T_0-TopSpace

    proof

      let T be non empty TopSpace;

      for x,y be Point of ( T_0-reflex T) st not x = y holds ex A be Subset of ( T_0-reflex T) st A is open & (x in A & not y in A or y in A & not x in A) by Lm1;

      hence thesis by Def7;

    end;

    theorem :: T_0TOPSP:10

    for T,S be non empty TopSpace st ex h be Function of ( T_0-reflex S), ( T_0-reflex T) st h is being_homeomorphism & (( T_0-canonical_map T),(h * ( T_0-canonical_map S))) are_fiberwise_equipotent holds (T,S) are_homeomorphic

    proof

      let T,S be non empty TopSpace;

      set F = ( T_0-canonical_map T), G = ( T_0-canonical_map S);

      set TR = ( T_0-reflex T), SR = ( T_0-reflex S);

      given h be Function of SR, TR such that

       A1: h is being_homeomorphism and

       A2: (F,(h * G)) are_fiberwise_equipotent ;

      consider f be Function such that

       A3: ( dom f) = ( dom F) and

       A4: ( rng f) = ( dom (h * G)) and

       A5: f is one-to-one and

       A6: F = ((h * G) * f) by A2, CLASSES1: 77;

      

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

      

       A8: h is continuous by A1;

      

       A9: h is one-to-one by A1;

      reconsider f as Function of T, S by A4, A7, FUNCT_2:def 1, RELSET_1: 4;

      take f;

      thus

       A10: ( dom f) = ( [#] T) & ( rng f) = ( [#] S) by A4, FUNCT_2:def 1;

      

       A11: ( rng h) = ( [#] TR) by A1;

      

       A12: ( [#] SR) <> {} ;

      

       A13: for A be Subset of S st A is open holds (f " A) is open

      proof

        set g = (h * G);

        let A be Subset of S;

        set B = (g .: A);

        

         A14: (h " ) is continuous by A1;

        assume

         A15: A is open;

        

         A16: for x1,x2 be Element of S holds x1 in A & (g . x1) = (g . x2) implies x2 in A

        proof

          let x1,x2 be Element of S;

          assume that

           A17: x1 in A and

           A18: (g . x1) = (g . x2);

          (h . (G . x1)) = (g . x2) by A18, FUNCT_2: 15;

          then (h . (G . x1)) = (h . (G . x2)) by FUNCT_2: 15;

          then (G . x1) = (G . x2) by A9, FUNCT_2: 19;

          hence thesis by A15, A17, Th6;

        end;

        G is open by Th8;

        then (G .: A) is open by A15;

        then

         A19: ((h " ) " (G .: A)) is open by A12, A14, TOPS_2: 43;

        

         A20: h is onto by A11, FUNCT_2:def 3;

        (h .: (G .: A)) = ((h qua Function " ) " (G .: A)) by A9, FUNCT_1: 84;

        then (h .: (G .: A)) is open by A9, A19, A20, TOPS_2:def 4;

        then

         A21: ((h * G) .: A) is open by RELAT_1: 126;

        ( [#] ( T_0-reflex T)) <> {} ;

        then

         A22: (F " B) is open by A21, TOPS_2: 43;

        (F " B) = (f " (g " (g .: A))) by A6, RELAT_1: 146;

        hence thesis by A22, A16, Th1;

      end;

      

       A23: ( dom h) = ( [#] SR) by A1;

      

       A24: for A be Subset of T st A is open holds ((f " ) qua Function of S, T " A) is open

      proof

        set g = ((h " ) * F);

        let A be Subset of T;

        set B = (g .: A);

        assume

         A25: A is open;

        

         A26: for x1,x2 be Element of T holds x1 in A & (g . x1) = (g . x2) implies x2 in A

        proof

          let x1,x2 be Element of T;

          assume that

           A27: x1 in A and

           A28: (g . x1) = (g . x2);

          ((h " ) . (F . x1)) = (g . x2) by A28, FUNCT_2: 15;

          then

           A29: ((h " ) . (F . x1)) = ((h " ) . (F . x2)) by FUNCT_2: 15;

          (h " ) is one-to-one by A11, A9, TOPS_2: 50;

          then (F . x1) = (F . x2) by A29, FUNCT_2: 19;

          hence thesis by A25, A27, Th6;

        end;

        F = (h * (G * f)) by A6, RELAT_1: 36;

        then g = (((h " ) * h) * (G * f)) by RELAT_1: 36;

        then g = (( id the carrier of SR) * (G * f)) by A23, A11, A9, TOPS_2: 52;

        then (g * (f " )) = ((G * f) * (f " )) by FUNCT_2: 17;

        then (g * (f " )) = (G * (f * (f " ))) by RELAT_1: 36;

        then (g * (f " )) = (G * ( id the carrier of S)) by A5, A10, TOPS_2: 52;

        then G = (g * (f " )) by FUNCT_2: 17;

        then

         A30: (G " B) = ((f " ) " (g " B)) by RELAT_1: 146;

        F is open by Th8;

        then (F .: A) is open by A25;

        then

         A31: (h " (F .: A)) is open by A11, A8, TOPS_2: 43;

        B = ((h " ) .: (F .: A)) by RELAT_1: 126;

        then (G " B) = (G " (h " (F .: A))) by A11, A9, TOPS_2: 55;

        then (G " B) is open by A12, A31, TOPS_2: 43;

        hence thesis by A26, A30, Th1;

      end;

      thus f is one-to-one by A5;

      ( [#] S) <> {} ;

      hence f is continuous by A13, TOPS_2: 43;

      ( [#] T) <> {} ;

      hence thesis by A24, TOPS_2: 43;

    end;

    theorem :: T_0TOPSP:11

    

     Th11: for T be non empty TopSpace, T0 be T_0-TopSpace, f be continuous Function of T, T0 holds for p,q be Point of T holds [p, q] in ( Indiscernibility T) implies (f . p) = (f . q)

    proof

      let T be non empty TopSpace;

      let T0 be T_0-TopSpace;

      let f be continuous Function of T, T0;

      let p,q be Point of T;

      set p9 = (f . p), q9 = (f . q);

      assume that

       A1: [p, q] in ( Indiscernibility T) and

       A2: not (f . p) = (f . q);

      consider V be Subset of T0 such that

       A3: V is open and

       A4: p9 in V & not q9 in V or q9 in V & not p9 in V by A2, Def7;

      set A = (f " V);

      ( [#] T0) <> {} ;

      then

       A5: A is open by A3, TOPS_2: 43;

      reconsider f as Function of the carrier of T, the carrier of T0;

      q in the carrier of T;

      then

       A6: q in ( dom f) by FUNCT_2:def 1;

      p in the carrier of T;

      then p in ( dom f) by FUNCT_2:def 1;

      then not (p in A iff q in A) by A4, A6, FUNCT_1:def 7;

      hence contradiction by A1, A5, Def3;

    end;

    theorem :: T_0TOPSP:12

    

     Th12: for T be non empty TopSpace, T0 be T_0-TopSpace, f be continuous Function of T, T0 holds for p be Point of T holds (f .: ( Class (( Indiscernibility T),p))) = {(f . p)}

    proof

      let T be non empty TopSpace;

      let T0 be T_0-TopSpace;

      let f be continuous Function of T, T0;

      let p be Point of T;

      set R = ( Indiscernibility T);

      for y be object holds y in (f .: ( Class (R,p))) iff y in {(f . p)}

      proof

        let y be object;

        hereby

          assume y in (f .: ( Class (R,p)));

          then

          consider x be object such that

           A1: x in the carrier of T and

           A2: x in ( Class (R,p)) and

           A3: y = (f . x) by FUNCT_2: 64;

           [x, p] in R by A2, EQREL_1: 19;

          then (f . x) = (f . p) by A1, Th11;

          hence y in {(f . p)} by A3, TARSKI:def 1;

        end;

        assume y in {(f . p)};

        then

         A4: y = (f . p) by TARSKI:def 1;

        p in ( Class (R,p)) by EQREL_1: 20;

        hence thesis by A4, FUNCT_2: 35;

      end;

      hence thesis by TARSKI: 2;

    end;

    theorem :: T_0TOPSP:13

    for T be non empty TopSpace, T0 be T_0-TopSpace, f be continuous Function of T, T0 holds ex h be continuous Function of ( T_0-reflex T), T0 st f = (h * ( T_0-canonical_map T))

    proof

      let T be non empty TopSpace;

      let T0 be T_0-TopSpace;

      let f be continuous Function of T, T0;

      set F = ( T_0-canonical_map T);

      set R = ( Indiscernibility T);

      set TR = ( T_0-reflex T);

      defpred X[ object, object] means ex D1 be set st D1 = $1 & $2 in (f .: D1);

      

       A1: for C be object st C in the carrier of TR holds ex y be object st y in the carrier of T0 & X[C, y]

      proof

        let C be object;

        assume C in the carrier of TR;

        then

        consider p be Point of T such that

         A2: C = ( Class (R,p)) by Th3;

        

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

        reconsider C as set by TARSKI: 1;

        (f .: C) = {(f . p)} by A2, Th12;

        hence thesis by A3;

      end;

      ex h be Function of the carrier of TR, the carrier of T0 st for C be object st C in the carrier of TR holds X[C, (h . C)] from FUNCT_2:sch 1( A1);

      then

      consider h be Function of the carrier of TR, the carrier of T0 such that

       A4: for C be object st C in the carrier of TR holds X[C, (h . C)];

      

       A5: for p be Point of T holds (h . ( Class (R,p))) = (f . p)

      proof

        let p be Point of T;

        ( Class (R,p)) is Point of TR by Th3;

        then X[( Class (R,p)), (h . ( Class (R,p)))] by A4;

        then (h . ( Class (R,p))) in (f .: ( Class (R,p)));

        then (h . ( Class (R,p))) in {(f . p)} by Th12;

        hence thesis by TARSKI:def 1;

      end;

      reconsider h as Function of TR, T0;

      

       A6: ( [#] T0) <> {} ;

      for W be Subset of T0 st W is open holds (h " W) is open

      proof

        let W be Subset of T0;

        assume W is open;

        then

         A7: (f " W) is open by A6, TOPS_2: 43;

        set V = (h " W);

        for x be object holds x in ( union V) iff x in (f " W)

        proof

          let x be object;

          hereby

            assume x in ( union V);

            then

            consider C be set such that

             A8: x in C and

             A9: C in V by TARSKI:def 4;

            consider p be Point of T such that

             A10: C = ( Class (R,p)) by A9, Th3;

            x in the carrier of T by A8, A10;

            then

             A11: x in ( dom f) by FUNCT_2:def 1;

             [x, p] in R by A8, A10, EQREL_1: 19;

            then

             A12: C = ( Class (R,x)) by A8, A10, EQREL_1: 35;

            (h . C) in W by A9, FUNCT_1:def 7;

            then (f . x) in W by A5, A8, A12;

            hence x in (f " W) by A11, FUNCT_1:def 7;

          end;

          assume

           A13: x in (f " W);

          then (f . x) in W by FUNCT_1:def 7;

          then

           A14: (h . ( Class (R,x))) in W by A5, A13;

          ( Class (R,x)) is Point of TR by A13, Th3;

          then

           A15: ( Class (R,x)) in V by A14, FUNCT_2: 38;

          x in ( Class (R,x)) by A13, EQREL_1: 20;

          hence thesis by A15, TARSKI:def 4;

        end;

        then ( union V) = (f " W) by TARSKI: 2;

        then ( union V) in the topology of T by A7;

        hence thesis by Th2;

      end;

      then

      reconsider h as continuous Function of TR, T0 by A6, TOPS_2: 43;

      set H = (h * F);

      for x be object st x in the carrier of T holds (f . x) = (H . x)

      proof

        let x be object;

        assume

         A16: x in the carrier of T;

        then ( Class (R,x)) in ( Class R) by EQREL_1:def 3;

        then

         A17: ( Class (R,x)) in the carrier of TR by BORSUK_1:def 7;

        x in ( dom F) & (F . x) = ( Class (R,x)) by A16, Th4, FUNCT_2:def 1;

        then

         A18: ((h * F) . x) = (h . ( Class (R,x))) by FUNCT_1: 13;

         X[( Class (R,x)), (h . ( Class (R,x)))] by A4, A17;

        then (H . x) in (f .: ( Class (R,x))) by A18;

        then (H . x) in {(f . x)} by A16, Th12;

        hence thesis by TARSKI:def 1;

      end;

      hence thesis by FUNCT_2: 12;

    end;