The Mizar article:

Retracts and Inheritance

by
Grzegorz Bancerek

Received September 7, 1999

Copyright (c) 1999 Association of Mizar Users

MML identifier: YELLOW16
[ MML identifier index ]


environ

 vocabulary RELAT_1, SEQ_1, ORDERS_1, YELLOW_0, FUNCT_1, CAT_1, RELAT_2,
      WAYBEL_0, SEQM_3, PRE_TOPC, FUNCOP_1, QUANTAL1, ORDINAL2, BINOP_1, BOOLE,
      GROUP_6, LATTICES, FUNCT_3, BORSUK_1, WAYBEL_1, WELLORD1, BHSP_3,
      YELLOW_1, WAYBEL_3, GROUP_1, CARD_3, PBOOLE, LATTICE3, FUNCT_4, RLVECT_2,
      SUBSET_1, WAYBEL18, YELLOW_9, T_0TOPSP, TOPS_2, YELLOW16;
 notation TARSKI, XBOOLE_0, ENUMSET1, ZFMISC_1, SUBSET_1, RELAT_1, FUNCT_1,
      PARTFUN1, FUNCT_2, FUNCT_3, FUNCT_7, STRUCT_0, CARD_3, ZF_FUND1, PBOOLE,
      PRALG_1, PRE_CIRC, FUNCT_4, WELLORD1, ORDERS_1, LATTICE3, GRCAT_1,
      PRE_TOPC, TOPS_2, T_0TOPSP, BORSUK_1, QUANTAL1, YELLOW_0, WAYBEL_0,
      YELLOW_1, YELLOW_2, WAYBEL_1, YELLOW_9, WAYBEL_3, WAYBEL18;
 constructors PRE_CIRC, FUNCT_7, ENUMSET1, ORDERS_3, WAYBEL_1, T_0TOPSP,
      ZF_FUND1, QUANTAL1, GRCAT_1, TOPS_2, YELLOW_9, NATTRA_1, TOLER_1,
      WAYBEL18, BORSUK_1;
 clusters STRUCT_0, WAYBEL_0, WAYBEL_3, RELSET_1, YELLOW_1, LATTICE3, BORSUK_2,
      WAYBEL10, WAYBEL17, YELLOW_0, FUNCT_1, SUBSET_1, PRE_TOPC, TOPS_1,
      YELLOW_2, WAYBEL18, XBOOLE_0;
 requirements SUBSET, BOOLE;
 definitions TARSKI, RELAT_1, LATTICE3, YELLOW_0, BORSUK_1, WAYBEL_0, YELLOW_1,
      YELLOW_2, WAYBEL_1, WAYBEL_3, T_0TOPSP, WAYBEL25, XBOOLE_0;
 theorems STRUCT_0, YELLOW_0, WAYBEL_0, YELLOW_1, YELLOW_2, WAYBEL_1, PRE_TOPC,
      BORSUK_1, TOPMETR, ORDERS_1, YELLOW12, ZF_FUND1, RELAT_1, FUNCT_2,
      FUNCT_1, ENUMSET1, WAYBEL_3, PBOOLE, FUNCOP_1, LATTICE3, CARD_3, TARSKI,
      ZFMISC_1, WELLORD1, GRCAT_1, QUANTAL1, FUNCT_4, YELLOW_9, WAYBEL20,
      FUNCT_7, TOPS_2, FUNCT_3, WAYBEL10, T_0TOPSP, WAYBEL15, YELLOW_6,
      PRALG_1, WAYBEL18, WAYBEL13, WAYBEL21, XBOOLE_0, XBOOLE_1, AMI_1;
 schemes PRALG_2;

begin :: Poset retracts

theorem
   for a,b being Relation holds a*b = a(#)b
  proof let a,b be Relation;
   thus a*b c= a(#)b
    proof let x be set; assume
A1:    x in a*b;
     then consider x1,x2 being set such that
A2:    x = [x1,x2] by RELAT_1:def 1;
        ex y being set st [x1,y] in a & [y,x2] in b by A1,A2,RELAT_1:def 8;
     hence thesis by A2,ZF_FUND1:def 1;
    end;
   let x be set; assume x in a(#)b;
    then ex u,v,w being set st x = [u,w] & [u,v] in a & [v,w] in
 b by ZF_FUND1:def 1;
   hence thesis by RELAT_1:def 8;
  end;

theorem
   for X being set, L being non empty RelStr, S being non empty SubRelStr of L
 for f,g being Function of X, the carrier of S
 for f',g' being Function of X, the carrier of L
  st f' = f & g' = g & f <= g
  holds f' <= g'
  proof let X be set, L be non empty RelStr, S be non empty SubRelStr of L;
   let f,g be Function of X, the carrier of S;
   let f',g' be Function of X, the carrier of L such that
A1:  f' = f & g' = g & f <= g;
   let x be set; assume
A2:  x in X;
    then f.x in the carrier of S & g.x in the carrier of S by FUNCT_2:7;
   then reconsider a = f.x, b = g.x as Element of S;
   reconsider a' = a, b' = b as Element of L by YELLOW_0:59;
   take a', b'; thus a' = f'.x & b' = g'.x by A1;
      ex a,b being Element of S st a = f.x & b = g.x & a <= b
     by A1,A2,YELLOW_2:def 1;
   hence thesis by YELLOW_0:60;
  end;

theorem
   for X being set, L being non empty RelStr
 for S being full non empty SubRelStr of L
 for f,g being Function of X, the carrier of S
 for f',g' being Function of X, the carrier of L
  st f' = f & g' = g & f' <= g'
  holds f <= g
  proof let X be set, L be non empty RelStr;
   let S be full non empty SubRelStr of L;
   let f,g be Function of X, the carrier of S;
   let f',g' be Function of X, the carrier of L such that
A1:  f' = f & g' = g & f' <= g';
   let x be set; assume
A2:  x in X;
  then f.x in the carrier of S & g.x in the carrier of S by FUNCT_2:7;
   then reconsider a = f.x, b = g.x as Element of S;
   take a, b; thus a = f.x & b = g.x;
      ex a',b' being Element of L st a' = a & b' = b & a' <= b'
     by A1,A2,YELLOW_2:def 1;
   hence thesis by YELLOW_0:61;
  end;

definition
 let S be non empty RelStr;
 let T be non empty reflexive antisymmetric RelStr;
 cluster directed-sups-preserving monotone map of S,T;
 existence
  proof consider x being Element of T;
   take f = S --> x;
A1:  f = (the carrier of S) --> x by BORSUK_1:def 3;
   thus f is directed-sups-preserving
     proof let X be Subset of S; assume
A2:    X is non empty directed;
A3:    f.:X = {x}
       proof thus f.:X c= {x} by A1,BORSUK_1:6;
        consider a being Element of X;
A4:       a in X by A2;
         then f.a = x & dom f = the carrier of S by A1,FUNCOP_1:13,19;
         then x in f.:X by A4,FUNCT_1:def 12;
        hence thesis by ZFMISC_1:37;
       end;
     assume ex_sup_of X,S;
     thus ex_sup_of f.:X, T by A3,YELLOW_0:38;
     thus sup (f.:X) = x by A3,YELLOW_0:39 .= f.sup X by A1,FUNCOP_1:13;
    end;
   let a,b be Element of S;
      f.a = x & f.b = x & x <= x by A1,FUNCOP_1:13;
   hence thesis;
  end;
end;

theorem
   for f,g being Function st f is idempotent & rng g c= rng f & rng g c= dom f
  holds f*g = g
  proof let f,g be Function; assume f is idempotent;
then A1:  f*f = f by QUANTAL1:def 9;
   assume
A2:  rng g c= rng f;
   assume
    rng g c= dom f;
then A3:  dom (f*g) = dom g by RELAT_1:46;
      now let x be set; assume x in dom g;
then A4:    (f*g).x = f.(g.x) & g.x in rng g by FUNCT_1:23,def 5;
     then consider a being set such that
A5:    a in dom f & g.x = f.a by A2,FUNCT_1:def 5;
     thus (f*g).x = g.x by A1,A4,A5,FUNCT_1:23;
    end;
   hence f*g = g by A3,FUNCT_1:9;
  end;

definition
 let S be 1-sorted;
 cluster idempotent map of S,S;
 existence
  proof take f = id S;
A1:  the carrier of S = {} implies the carrier of S = {};
      f = id the carrier of S by GRCAT_1:def 11;
    then f*f = f by A1,FUNCT_2:23;
   hence thesis by QUANTAL1:def 9;
  end;
end;

theorem Th5:
 for L being up-complete (non empty Poset)
 for S being directed-sups-inheriting full (non empty SubRelStr of L)
  holds S is up-complete
  proof let L be up-complete (non empty Poset);
   let S be directed-sups-inheriting full (non empty SubRelStr of L);
      now let X be non empty directed Subset of S;
     reconsider Y = X as non empty directed Subset of L by YELLOW_2:7;
        ex_sup_of Y,L by WAYBEL_0:75;
     hence ex_sup_of X,S by WAYBEL_0:7;
    end;
   hence S is up-complete by WAYBEL_0:75;
  end;

theorem Th6:
 for L being up-complete (non empty Poset)
 for f being map of L, L st f is idempotent directed-sups-preserving
  holds Image f is directed-sups-inheriting
  proof let L be up-complete (non empty Poset);
   let f be map of L, L;
   assume
A1: f is idempotent directed-sups-preserving;
   set S = subrelstr(rng f);
   consider a being Element of L;
      dom f = the carrier of L by FUNCT_2:def 1;
    then f.a in rng f by FUNCT_1:def 5;
    then the carrier of S is non empty by YELLOW_0:def 15;
   then reconsider S' = S as non empty full SubRelStr of L by STRUCT_0:def 1;
      S is directed-sups-inheriting
     proof
      let X be directed Subset of S;
      assume X <> {};
       then X is non empty directed Subset of S';
      then reconsider X'= X as non empty directed Subset of L by YELLOW_2:7;
A2:    f preserves_sup_of X' by A1,WAYBEL_0:def 37;
      assume ex_sup_of X,L;
then A3:    ex_sup_of f.:X',L & sup(f.:X') = f.sup X' by A2,WAYBEL_0:def 31;
         X c= the carrier of S;
       then X c= rng f by YELLOW_0:def 15;
       then sup X' = f.sup X' & the carrier of L <> {} by A1,A3,YELLOW_2:22;
       then "\/"(X, L) in rng f by FUNCT_2:6;
      hence "\/"(X, L) in the carrier of S by YELLOW_0:def 15;
     end;
   hence Image f is directed-sups-inheriting by YELLOW_2:def 2;
  end;

canceled;

theorem Th8:
 for S, T being non empty RelStr, f being map of T,S, g being map of S,T holds
   f*g = id S implies rng f = the carrier of S
  proof let S,T be non empty RelStr;
   let f be map of T,S, g be map of S,T such that
A1:  f*g = id S;
      id S = id the carrier of S & the carrier of T <> {} by GRCAT_1:def 11;
   hence rng f = the carrier of S by A1,FUNCT_2:29;
  end;

theorem Th9:
 for T being non empty RelStr, S being non empty SubRelStr of T
 for f being map of T,S holds
   f*incl(S,T) = id S implies f is idempotent map of T, T
  proof let T be non empty RelStr, S be non empty SubRelStr of T;
   let f be map of T,S; assume
A1:  f*incl(S, T) = id S;
then A2:  rng f = the carrier of S by Th8;
A3:  the carrier of S c= the carrier of T by YELLOW_0:def 13;
    then incl(S, T) = id the carrier of S by YELLOW_9:def 1;
    then incl(S, T)*f = f by FUNCT_2:23;
    then A4: f*f = (id S)*f by A1,RELAT_1:55
       .= (id the carrier of S)*f by GRCAT_1:def 11
       .= f by FUNCT_2:23;
      dom f = the carrier of T by FUNCT_2:def 1;
    then f is Function of the carrier of T, the carrier of T by A2,A3,FUNCT_2:4
;
   hence thesis by A4,QUANTAL1:def 9;
  end;

definition
 let S,T be non empty Poset;
 let f be Function;
 pred f is_a_retraction_of T,S means:Def1:
  f is directed-sups-preserving map of T,S & f|the carrier of S = id S &
  S is directed-sups-inheriting full SubRelStr of T;

 pred f is_an_UPS_retraction_of T,S means:Def2:
  f is directed-sups-preserving map of T,S &
  ex g being directed-sups-preserving map of S,T st f*g = id S;
end;

definition
 let S,T be non empty Poset;
 pred S is_a_retract_of T means:Def3:
  ex f being map of T,S st f is_a_retraction_of T,S;

 pred S is_an_UPS_retract_of T means:Def4:
  ex f being map of T,S st f is_an_UPS_retraction_of T,S;
end;

theorem Th10:
 for S,T being non empty Poset, f being Function
  st f is_a_retraction_of T,S
  holds f*incl(S,T) = id S
  proof let S,T be non empty Poset, f be Function such that
      f is directed-sups-preserving map of T,S and
A1:  f|the carrier of S = id S and
A2:  S is directed-sups-inheriting full SubRelStr of T;
      the carrier of S c= the carrier of T by A2,YELLOW_0:def 13;
   hence f*incl(S, T) = f*id the carrier of S by YELLOW_9:def 1
      .= id S by A1,RELAT_1:94;
  end;

theorem Th11:
 for S being non empty Poset, T being up-complete (non empty Poset)
 for f being Function
  st f is_a_retraction_of T,S
  holds f is_an_UPS_retraction_of T,S
  proof let S be non empty Poset;
   let T be up-complete (non empty Poset), f be Function; assume
A1:  f is_a_retraction_of T,S;
   hence f is directed-sups-preserving map of T,S by Def1;
      S is directed-sups-inheriting full SubRelStr of T by A1,Def1;
   then reconsider g = incl(S,T) as directed-sups-preserving map of S,T
     by WAYBEL21:10;
   take g; thus f*g = id S by A1,Th10;
  end;

theorem Th12:
 for S,T being non empty Poset, f being Function
  st f is_a_retraction_of T,S
 holds rng f = the carrier of S
  proof let S,T be non empty Poset, f be Function; assume
      f is_a_retraction_of T,S;
    then f*incl(S,T) = id S & f is map of T,S by Def1,Th10;
   hence thesis by Th8;
  end;

theorem Th13:
 for S,T being non empty Poset, f being Function
  st f is_an_UPS_retraction_of T,S
 holds rng f = the carrier of S
  proof let S,T be non empty Poset, f be Function; assume
      f is directed-sups-preserving map of T,S &
    ex g being directed-sups-preserving map of S,T st f*g = id S;
   hence thesis by Th8;
  end;

theorem Th14:
 for S,T being non empty Poset, f being Function
  st f is_a_retraction_of T,S
 holds f is idempotent map of T,T
  proof let S,T be non empty Poset, f be Function; assume
      f is_a_retraction_of T,S;
    then f*incl(S,T) = id S & f is map of T,S & S is SubRelStr of T by Def1,
Th10;
   hence thesis by Th9;
  end;

theorem Th15:
 for T,S being non empty Poset, f being map of T,T
  st f is_a_retraction_of T,S
  holds Image f = the RelStr of S
  proof let T,S be non empty Poset, f be map of T,T; assume
      f is_a_retraction_of T,S;
then A1:  rng f = the carrier of S & S is full SubRelStr of T by Def1,Th12;
      Image f = subrelstr rng f by YELLOW_2:def 2;
    then the carrier of Image f = rng f by YELLOW_0:def 15;
   hence thesis by A1,YELLOW_0:58;
  end;

theorem Th16:
 for T being up-complete (non empty Poset)
 for S being non empty Poset, f being map of T,T
  st f is_a_retraction_of T,S
  holds f is directed-sups-preserving projection
  proof let T be up-complete (non empty Poset);
   let S be non empty Poset, f be map of T,T; assume
A1:  f is_a_retraction_of T,S;
   then reconsider g = f as directed-sups-preserving map of T,S by Def1;
A2:  f is_an_UPS_retraction_of T,S by A1,Th11;
   f is idempotent by A1,Th14;
then A3:  f = f*f by QUANTAL1:def 9 .= (f|rng f)*f by FUNCT_4:2
     .= (f|the carrier of S)*f by A2,Th13 .= (id S)*f by A1,Def1
     .= (id the carrier of S)*g by GRCAT_1:def 11;
A4:  S is full directed-sups-inheriting non empty SubRelStr of T
     by A1,Def1;
then A5:  incl(S,T) is directed-sups-preserving by WAYBEL21:10;
      the carrier of S c= the carrier of T by A4,YELLOW_0:def 13;
    then A6: incl(S,T) = id the carrier of S by YELLOW_9:def 1;
   hence f is directed-sups-preserving by A3,A5,WAYBEL20:29;
      f is directed-sups-preserving idempotent map of T,T by A1,A3,A5,A6,Th14,
WAYBEL20:29;
   hence thesis by WAYBEL_1:def 13;
  end;

theorem Th17:
 for S,T being non empty reflexive transitive RelStr
 for f being map of S,T holds
   f is isomorphic iff f is monotone &
      ex g being monotone map of T,S st f*g = id T & g*f = id S
  proof let S,T be non empty reflexive transitive RelStr, f be map of S,T;
A1:  id S = id the carrier of S & id T = id the carrier of T by GRCAT_1:def 11;
   hereby assume
A2:   f is isomorphic;
    hence f is monotone by WAYBEL_0:def 38;
    consider g being map of T,S such that
A3:   g = f qua Function" & g is monotone by A2,WAYBEL_0:def 38;
    reconsider g as monotone map of T,S by A3;
    take g;
       f is one-to-one & rng f = the carrier of T
      by A2,WAYBEL_0:66;
    hence f*g = id T & g*f = id S by A1,A3,FUNCT_2:35;
   end;
   assume
A4:  f is monotone;
   given g being monotone map of T,S such that
A5:  f*g = id T & g*f = id S;
A6:  f is one-to-one & rng f = the carrier of T by A1,A5,FUNCT_2:29;
    then g = f qua Function" by A1,A5,FUNCT_2:36;
   hence f is isomorphic by A4,A6,WAYBEL_0:def 38;
  end;

theorem Th18:
 for S,T being non empty Poset holds
   S,T are_isomorphic iff
      ex f being monotone map of S,T, g being monotone map of T,S
       st f*g = id T & g*f = id S
  proof let S,T be non empty Poset;
A1:  id S = id the carrier of S & id T = id the carrier of T by GRCAT_1:def 11;
   hereby assume S,T are_isomorphic;
    then consider f being map of S,T such that
A2:   f is isomorphic by WAYBEL_1:def 8;
    reconsider f as monotone map of S,T by A2,WAYBEL_0:def 38;
    take f;
    consider g being map of T,S such that
A3:   g = f qua Function" & g is monotone by A2,WAYBEL_0:def 38;
    reconsider g as monotone map of T,S by A3;
    take g;
       f is one-to-one & rng f = the carrier of T
      by A2,WAYBEL_0:66;
    hence f*g = id T & g*f = id S by A1,A3,FUNCT_2:35;
   end;
   given f being monotone map of S,T, g being monotone map of T,S such that
A4:  f*g = id T & g*f = id S;
   take f;
A5:  f is one-to-one & rng f = the carrier of T by A1,A4,FUNCT_2:29;
    then g = f qua Function" by A1,A4,FUNCT_2:36;
   hence f is isomorphic by A5,WAYBEL_0:def 38;
  end;

theorem
   for S,T being up-complete (non empty Poset)
  st S,T are_isomorphic
  holds S is_an_UPS_retract_of T & T is_an_UPS_retract_of S
  proof let S,T be up-complete (non empty Poset);
   assume S,T are_isomorphic;
   then consider f be monotone map of S,T, g be monotone map of T,S such that
A1:  f*g = id T & g*f = id S by Th18;
      f is isomorphic & g is isomorphic by A1,Th17;
    then f is sups-preserving & g is sups-preserving by WAYBEL13:20;
    then (for X being Subset of S st X is non empty directed
      holds f preserves_sup_of X) &
    for X being Subset of T st X is non empty directed
     holds g preserves_sup_of X by WAYBEL_0:def 33;
    then f is directed-sups-preserving & g is directed-sups-preserving
     by WAYBEL_0:def 37;
    then g is_an_UPS_retraction_of T,S &
    f is_an_UPS_retraction_of S,T by A1,Def2;
   hence thesis by Def4;
  end;

theorem Th20:
 for T,S being non empty Poset
 for f being monotone map of T,S, g being monotone map of S,T
  st f*g = id S
  ex h being projection map of T,T
   st h = g*f &
      h|the carrier of Image h = id Image h &
      S, Image h are_isomorphic
  proof let T,S be non empty Poset;
   let f be monotone map of T,S, g be monotone map of S,T such that
A1:  f*g = id S;
   set h = g*f;
A2:  id S = id the carrier of S by GRCAT_1:def 11;
      h*h = h*g*f by RELAT_1:55 .= g*(id S)*f by A1,RELAT_1:55
       .= h by A2,FUNCT_2:23;
    then h is idempotent monotone map of T,T by QUANTAL1:def 9,YELLOW_2:14;
   then reconsider h as projection map of T,T by WAYBEL_1:def 13;
   take h; thus h = g*f;
      id the carrier of Image h = id Image h by GRCAT_1:def 11;
   hence h|the carrier of Image h = h*id Image h by RELAT_1:94
      .= h*(inclusion h) by WAYBEL_1:def 17
      .= (corestr h)*(inclusion h) by WAYBEL_1:32
      .= id Image h by WAYBEL_1:36;
    rng f = the carrier of S & dom g = the carrier of S
     by A1,Th8,FUNCT_2:def 1;
then A4:  rng h = rng g by RELAT_1:47;
A5:  Image h = subrelstr rng h & Image g = subrelstr rng g
     by YELLOW_2:def 2;
   then reconsider gg = corestr g as map of S, Image h by A4;
   take gg;
A6:  gg = g by WAYBEL_1:32;
then A7:  gg is one-to-one by A1,A2,FUNCT_2:29;
A8:  rng gg = the carrier of Image h by A4,A5,A6,YELLOW_0:def 15;
      now let x,y be Element of S;
        x <= y implies g.x <= g.y & gg.x in the carrier of Image h
       by WAYBEL_1:def 2;
     hence x <= y implies gg.x <= gg.y by A6,YELLOW_0:61;
     assume gg.x <= gg.y;
then A9:    g.x <= g.y by A6,YELLOW_0:60;
        (id S).x = x & (id S).y = y by GRCAT_1:11;
      then x = f.(g.x) & y = f.(g.y) by A1,FUNCT_2:21;
     hence x <= y by A9,WAYBEL_1:def 2;
    end;
   hence gg is isomorphic by A7,A8,WAYBEL_0:66;
  end;

theorem Th21:
 for T being up-complete (non empty Poset), S being non empty Poset
 for f being Function st f is_an_UPS_retraction_of T,S
  ex h being directed-sups-preserving projection map of T,T
   st h is_a_retraction_of T, Image h & S, Image h are_isomorphic
  proof let T be up-complete (non empty Poset);
   let S be non empty Poset, f be Function such that
A1:  f is directed-sups-preserving map of T,S;
   given g being directed-sups-preserving map of S,T such that
A2:  f*g = id S;
   reconsider f as directed-sups-preserving map of T,S by A1;
   consider h being projection map of T,T such that
A3:  h = g*f and
A4:  h|the carrier of Image h = id Image h and
A5:  S, Image h are_isomorphic by A2,Th20;
   reconsider h as directed-sups-preserving projection map of T,T
     by A3,WAYBEL20:29;
   take h;
   reconsider R = Image h as non empty Poset;
      h = corestr h by WAYBEL_1:32;
then A6:  h is directed-sups-preserving map of T, R by WAYBEL20:22;
    R is directed-sups-inheriting full SubRelStr of T by Th6;
   hence h is_a_retraction_of T, Image h by A4,A6,Def1;
   thus thesis by A5;
  end;

theorem Th22:
 for L being up-complete (non empty Poset)
 for S being non empty Poset st S is_a_retract_of L
  holds S is up-complete
  proof let L be up-complete (non empty Poset);
   let S be non empty Poset;
   given f being map of L,S such that
A1:  f is_a_retraction_of L,S;
      S is full directed-sups-inheriting (non empty SubRelStr of L) by A1,Def1;
   hence thesis by Th5;
  end;

theorem Th23:
 for L being complete (non empty Poset)
 for S being non empty Poset st S is_a_retract_of L
  holds S is complete
  proof let L be complete (non empty Poset);
   let S be non empty Poset;
   given f being map of L, S such that
A1:  f is_a_retraction_of L,S;
   reconsider f as directed-sups-preserving projection map of L,L
     by A1,Th14,Th16;
      the RelStr of S = Image f & Image f is complete by A1,Th15,YELLOW_2:37;
   hence thesis by YELLOW_0:3;
  end;

theorem Th24:
 for L being continuous complete LATTICE
 for S being non empty Poset st S is_a_retract_of L
  holds S is continuous
  proof let L be continuous complete LATTICE;
   let S be non empty Poset; given f being map of L,S such that
A1:  f is_a_retraction_of L,S;
   reconsider g = f as directed-sups-preserving projection map of L,L
     by A1,Th14,Th16;
A2:  Image g is continuous LATTICE by WAYBEL15:17;
      Image g = the RelStr of S by A1,Th15;
   hence S is continuous by A2,YELLOW12:15;
  end;

theorem
   for L being up-complete (non empty Poset)
 for S being non empty Poset st S is_an_UPS_retract_of L
  holds S is up-complete
  proof let L be up-complete (non empty Poset);
   let S be non empty Poset;
   given f being map of L,S such that
A1:  f is_an_UPS_retraction_of L,S;
   consider h being directed-sups-preserving projection map of L,L such that
A2:  h is_a_retraction_of L, Image h & S, Image h are_isomorphic by A1,Th21;
      h = corestr h by WAYBEL_1:32;
    then Image h is_a_retract_of L by A2,Def3;
    then Image h is up-complete & Image h, S are_isomorphic by A2,Th22,WAYBEL_1
:7;
   hence thesis by WAYBEL13:30;
  end;

theorem
   for L being complete (non empty Poset)
 for S being non empty Poset st S is_an_UPS_retract_of L
  holds S is complete
  proof let L be complete (non empty Poset), S be non empty Poset;
   given f being map of L, S such that
A1:  f is_an_UPS_retraction_of L,S;
   consider h being directed-sups-preserving projection map of L,L such that
A2:  h is_a_retraction_of L, Image h & S, Image h are_isomorphic by A1,Th21;
      h = corestr h by WAYBEL_1:32;
    then Image h is_a_retract_of L by A2,Def3;
    then Image h is complete & Image h, S are_isomorphic by A2,Th23,WAYBEL_1:7
;
   hence thesis by WAYBEL20:18;
  end;

theorem
   for L being continuous complete LATTICE
 for S being non empty Poset st S is_an_UPS_retract_of L
  holds S is continuous
  proof let L be continuous complete LATTICE;
   let S be non empty Poset; given f being map of L,S such that
A1:  f is_an_UPS_retraction_of L,S;
   consider h being directed-sups-preserving projection map of L,L such that
A2:  h is_a_retraction_of L, Image h & S, Image h are_isomorphic by A1,Th21;
      h = corestr h by WAYBEL_1:32;
    then Image h is_a_retract_of L by A2,Def3;
    then Image h is continuous & Image h, S are_isomorphic by A2,Th24,WAYBEL_1:
7;
   hence thesis by WAYBEL15:11;
  end;

theorem Th28:
 for L being RelStr
 for S being full SubRelStr of L
 for R being SubRelStr of S
 holds R is full iff R is full SubRelStr of L
  proof let L be RelStr, S be full SubRelStr of L, R be SubRelStr of S;
   reconsider R' = R as SubRelStr of L by YELLOW_6:16;
A1:  the carrier of R c= the carrier of S by YELLOW_0:def 13;
   hereby assume R is full;
     then the InternalRel of R = (the InternalRel of S)|_2 the carrier of R
      by YELLOW_0:def 14
        .= ((the InternalRel of L)|_2 the carrier of S)|_2 the carrier of R
      by YELLOW_0:def 14
        .= (the InternalRel of L)|_2 the carrier of R' by A1,WELLORD1:29;
    hence R is full SubRelStr of L by YELLOW_0:def 14;
   end;
   assume
A2:  R is full SubRelStr of L;
      ((the InternalRel of L)|_2 the carrier of S)|_2 the carrier of R
        = (the InternalRel of L)|_2 the carrier of R by A1,WELLORD1:29
       .= the InternalRel of R by A2,YELLOW_0:def 14;
   hence the InternalRel of R = (the InternalRel of S)|_2 the carrier of R
        by YELLOW_0:def 14;
  end;

theorem
   for L being non empty transitive RelStr
 for S being directed-sups-inheriting non empty full SubRelStr of L
 for R being directed-sups-inheriting non empty SubRelStr of S
  holds R is directed-sups-inheriting SubRelStr of L
  proof let L be non empty transitive RelStr;
   let S be directed-sups-inheriting non empty full SubRelStr of L;
   let R be directed-sups-inheriting non empty SubRelStr of S;
   reconsider T = R as SubRelStr of L by YELLOW_6:16;
      T is directed-sups-inheriting
     proof let X be directed Subset of T;
      reconsider Y = X as directed Subset of S by YELLOW_2:7;
      assume
A1:     X <> {};
      assume ex_sup_of X,L;
       then sup Y = "\/"(X,L) & ex_sup_of Y, S by A1,WAYBEL_0:7;
      hence "\/"(X,L) in the carrier of T by A1,WAYBEL_0:def 4;
     end;
   hence thesis;
  end;

theorem
   for L being up-complete (non empty Poset)
 for S1,S2 being directed-sups-inheriting full non empty SubRelStr of L
  st S1 is SubRelStr of S2
 holds S1 is directed-sups-inheriting full SubRelStr of S2
  proof let L be up-complete (non empty Poset);
   let S1,S2 be directed-sups-inheriting full non empty SubRelStr of L;
   assume S1 is SubRelStr of S2;
   then reconsider S = S1 as SubRelStr of S2;
      S is directed-sups-inheriting
     proof let X be directed Subset of S; assume X <> {};
      then reconsider Y1 = X as non empty directed Subset of S1;
      reconsider Y = Y1 as non empty directed Subset of L by YELLOW_2:7;
      reconsider Y2 = Y1 as non empty directed Subset of S2 by YELLOW_2:7;
         ex_sup_of Y, L by WAYBEL_0:75;
       then sup Y2 = sup Y & sup Y = sup Y1 by WAYBEL_0:7;
       then sup Y2 in the carrier of S1;
      hence thesis;
     end;
   hence thesis by Th28;
  end;

begin :: Products

definition
 let R be Relation;
 attr R is Poset-yielding means:Def5:
  for x being set st x in rng R holds x is Poset;
end;

definition
 cluster Poset-yielding -> RelStr-yielding reflexive-yielding Relation;
 coherence
  proof let R be Relation; assume
A1:  for x being set st x in rng R holds x is Poset;
   hence for x being set st x in rng R holds x is RelStr;
   thus for S being RelStr st S in rng R holds S is reflexive by A1;
  end;
end;

definition
 let X be non empty set;
 let L be non empty RelStr;
 let i be Element of X;
 let Y be Subset of L|^X;
 redefine func pi(Y,i) -> Subset of L;
 coherence
  proof
   reconsider Y' = Y as Subset of product (X --> L) by YELLOW_1:def 5;
      pi(Y',i) is Subset of (X --> L).i;
   hence thesis by FUNCOP_1:13;
  end;
end;

definition
 let X be set;
 let S be Poset;
 cluster X --> S -> Poset-yielding;
 coherence
  proof
A1:  rng (X --> S) c= {S} by FUNCOP_1:19;
   let x be set; assume x in rng (X --> S);
   hence thesis by A1,TARSKI:def 1;
  end;
end;

definition
 let I be set;
 cluster Poset-yielding non-Empty ManySortedSet of I;
 existence
  proof consider P being non empty Poset;
   take I --> P; thus thesis;
  end;
end;

definition
 let I be non empty set;
 let J be Poset-yielding non-Empty ManySortedSet of I;
 cluster product J -> transitive antisymmetric;
 coherence
  proof
A1:  now let i be Element of I;
        dom J = I by PBOOLE:def 3;
      then J.i in rng J by FUNCT_1:def 5;
     hence J.i is Poset by Def5;
    end;
    then for i being Element of I holds J.i is transitive;
   hence product J is transitive by WAYBEL_3:29;
      for i being Element of I holds J.i is antisymmetric by A1;
   hence thesis by WAYBEL_3:30;
  end;
end;

definition
 let I be non empty set;
 let J be Poset-yielding non-Empty ManySortedSet of I;
 let i be Element of I;
 redefine func J.i -> non empty Poset;
 coherence
  proof dom J = I by PBOOLE:def 3;
    then J.i in rng J by FUNCT_1:def 5;
   hence thesis by Def5;
  end;
end;

Lm1:
  now let I be non empty set;
   let J be Poset-yielding non-Empty ManySortedSet of I;
   let X be Subset of product J;
   deffunc F(Element of I) = sup pi(X,$1);
   consider f being ManySortedSet of I such that
A1: for i being Element of I holds f.i = F(i) from LambdaDMS;
A2: dom f = I by PBOOLE:def 3;
      now let i be Element of I;
        f.i = sup pi(X,i) by A1;
     hence f.i is Element of J.i;
    end;
   then reconsider f as Element of product J by A2,WAYBEL_3:27;
   assume
A3: for i being Element of I holds ex_sup_of pi(X,i), J.i;
   take f;
   thus for i being Element of I holds f.i = sup pi(X,i) by A1;
   thus f is_>=_than X
     proof let x be Element of product J such that
A4:    x in X;
         now let i be Element of I;
           ex_sup_of pi(X,i), J.i & f.i = sup pi(X,i) by A1,A3;
         then f.i is_>=_than pi(X,i) & x.i in pi(X,i)
          by A4,CARD_3:def 6,YELLOW_0:30;
        hence x.i <= f.i by LATTICE3:def 9;
       end;
      hence thesis by WAYBEL_3:28;
     end;
   let g be Element of product J; assume
A5: X is_<=_than g;
      now let i be Element of I;
A6:   f.i = sup pi(X,i) & ex_sup_of pi(X,i), J.i by A1,A3;
        g.i is_>=_than pi(X,i)
       proof let a be Element of J.i; assume
           a in pi(X,i);
        then consider h being Function such that
A7:      h in X & a = h.i by CARD_3:def 6;
        reconsider h as Element of product J by A7;
           h <= g by A5,A7,LATTICE3:def 9;
        hence a <= g.i by A7,WAYBEL_3:28;
       end;
     hence f.i <= g.i by A6,YELLOW_0:30;
    end;
   hence f <= g by WAYBEL_3:28;
  end;

Lm2:
  now let I be non empty set;
   let J be Poset-yielding non-Empty ManySortedSet of I;
   let X be Subset of product J;
   deffunc F(Element of I) = inf pi(X,$1);
   consider f being ManySortedSet of I such that
A1: for i being Element of I holds f.i = F(i) from LambdaDMS;
A2: dom f = I by PBOOLE:def 3;
      now let i be Element of I;
        f.i = inf pi(X,i) by A1;
     hence f.i is Element of J.i;
    end;
   then reconsider f as Element of product J by A2,WAYBEL_3:27;
   assume
A3: for i being Element of I holds ex_inf_of pi(X,i), J.i;
   take f;
   thus for i being Element of I holds f.i = inf pi(X,i) by A1;
   thus f is_<=_than X
     proof let x be Element of product J such that
A4:    x in X;
         now let i be Element of I;
           ex_inf_of pi(X,i), J.i & f.i = inf pi(X,i) by A1,A3;
         then f.i is_<=_than pi(X,i) & x.i in pi(X,i)
          by A4,CARD_3:def 6,YELLOW_0:31;
        hence x.i >= f.i by LATTICE3:def 8;
       end;
      hence thesis by WAYBEL_3:28;
     end;
   let g be Element of product J; assume
A5: X is_>=_than g;
      now let i be Element of I;
A6:   f.i = inf pi(X,i) & ex_inf_of pi(X,i), J.i by A1,A3;
        g.i is_<=_than pi(X,i)
       proof let a be Element of J.i; assume
           a in pi(X,i);
        then consider h being Function such that
A7:      h in X & a = h.i by CARD_3:def 6;
        reconsider h as Element of product J by A7;
           h >= g by A5,A7,LATTICE3:def 8;
        hence a >= g.i by A7,WAYBEL_3:28;
       end;
     hence f.i >= g.i by A6,YELLOW_0:31;
    end;
   hence f >= g by WAYBEL_3:28;
  end;

theorem Th31:
 for I being non empty set
 for J being Poset-yielding non-Empty ManySortedSet of I
 for f being Element of product J, X being Subset of product J
  holds
   f is_>=_than X
     iff for i being Element of I holds f.i is_>=_than pi(X,i)
  proof let I be non empty set;
   let J be Poset-yielding non-Empty ManySortedSet of I;
   let f be Element of product J, X be Subset of product J;
   hereby assume
A1:  f is_>=_than X;
    let i be Element of I;
    thus f.i is_>=_than pi(X, i)
      proof let x be Element of J.i; assume
       x in pi(X, i);
       then consider g being Function such that
A2:     g in X & x = g.i by CARD_3:def 6;
       reconsider g as Element of product J by A2;
          g <= f by A1,A2,LATTICE3:def 9;
       hence thesis by A2,WAYBEL_3:28;
      end;
   end;
   assume
A3: for i being Element of I holds f.i is_>=_than pi(X,i);
   let g be Element of product J; assume
A4: g in X;
      now let i be Element of I;
        g.i in pi(X,i) & f.i is_>=_than pi(X,i) by A3,A4,CARD_3:def 6;
     hence g.i <= f.i by LATTICE3:def 9;
    end;
   hence thesis by WAYBEL_3:28;
  end;

theorem Th32:
 for I being non empty set
 for J being Poset-yielding non-Empty ManySortedSet of I
 for f being Element of product J, X being Subset of product J
  holds
   f is_<=_than X
     iff for i being Element of I holds f.i is_<=_than pi(X,i)
  proof let I be non empty set;
   let J be Poset-yielding non-Empty ManySortedSet of I;
   let f be Element of product J, X be Subset of product J;
   hereby assume
A1:  f is_<=_than X;
    let i be Element of I;
    thus f.i is_<=_than pi(X, i)
      proof let x be Element of J.i; assume
       x in pi(X, i);
       then consider g being Function such that
A2:     g in X & x = g.i by CARD_3:def 6;
       reconsider g as Element of product J by A2;
          g >= f by A1,A2,LATTICE3:def 8;
       hence thesis by A2,WAYBEL_3:28;
      end;
   end;
   assume
A3: for i being Element of I holds f.i is_<=_than pi(X,i);
   let g be Element of product J; assume
A4: g in X;
      now let i be Element of I;
        g.i in pi(X,i) & f.i is_<=_than pi(X,i) by A3,A4,CARD_3:def 6;
     hence g.i >= f.i by LATTICE3:def 8;
    end;
   hence thesis by WAYBEL_3:28;
  end;

theorem Th33:
 for I being non empty set
 for J being Poset-yielding non-Empty ManySortedSet of I
 for X being Subset of product J
  holds
   ex_sup_of X, product J
     iff for i being Element of I holds ex_sup_of pi(X,i), J.i
  proof let I be non empty set;
   let J be Poset-yielding non-Empty ManySortedSet of I;
   let X be Subset of product J;
   hereby assume
A1:  ex_sup_of X, product J;
    let i be Element of I; set f = sup X;
       f is_>=_than X by A1,YELLOW_0:30;
then A2:  f.i is_>=_than pi(X, i) by Th31;
       now let x be Element of J.i; assume
A3:    pi(X,i) is_<=_than x;
      set g = f+*(i,x);
A4:    dom g = dom f & dom f = I by FUNCT_7:32,WAYBEL_3:27;
then A5:    g.i = x by FUNCT_7:33;
         now let j be Element of I;
           g.j = f.j or g.j = x & j = i by A5,FUNCT_7:34;
        hence g.j is Element of J.j;
       end;
      then reconsider g as Element of product J by A4,WAYBEL_3:27;
A6:    X is_<=_than f by A1,YELLOW_0:30;
         X is_<=_than g
        proof let h be Element of product J; assume h in X;
then A7:       h <= f & h.i in pi(X, i) by A6,CARD_3:def 6,LATTICE3:def 9;
            now let j be Element of I;
              g.j = f.j or g.j = x & j = i by A5,FUNCT_7:34;
           hence h.j <= g.j by A3,A7,LATTICE3:def 9,WAYBEL_3:28;
          end;
         hence h <= g by WAYBEL_3:28;
        end;
       then f <= g by A1,YELLOW_0:30;
      hence f.i <= x by A5,WAYBEL_3:28;
     end;
    hence ex_sup_of pi(X, i), J.i by A2,YELLOW_0:30;
   end;
   assume for i being Element of I holds ex_sup_of pi(X,i), J.i;
   then consider f being Element of product J such that
      for i being Element of I holds f.i = sup pi(X,i) and
A8: f is_>=_than X and
A9: for g being Element of product J st X is_<=_than g holds f <= g by Lm1;
   thus ex_sup_of X, product J by A8,A9,YELLOW_0:30;
  end;

theorem Th34:
 for I being non empty set
 for J being Poset-yielding non-Empty ManySortedSet of I
 for X being Subset of product J
  holds
   ex_inf_of X, product J
     iff for i being Element of I holds ex_inf_of pi(X,i), J.i
  proof let I be non empty set;
   let J be Poset-yielding non-Empty ManySortedSet of I;
   let X be Subset of product J;
   hereby assume
A1:  ex_inf_of X, product J;
    let i be Element of I; set f = inf X;
A2:  f is_<=_than X by A1,YELLOW_0:31;
then A3:  f.i is_<=_than pi(X, i) by Th32;
       now let x be Element of J.i; assume
A4:    pi(X,i) is_>=_than x;
      set g = f+*(i,x);
A5:    dom g = dom f & dom f = I by FUNCT_7:32,WAYBEL_3:27;
then A6:    g.i = x by FUNCT_7:33;
         now let j be Element of I;
           g.j = f.j or g.j = x & j = i by A6,FUNCT_7:34;
        hence g.j is Element of J.j;
       end;
      then reconsider g as Element of product J by A5,WAYBEL_3:27;
         X is_>=_than g
        proof let h be Element of product J; assume h in X;
then A7:       h >= f & h.i in pi(X, i) by A2,CARD_3:def 6,LATTICE3:def 8;
            now let j be Element of I;
              g.j = f.j or g.j = x & j = i by A6,FUNCT_7:34;
           hence h.j >= g.j by A4,A7,LATTICE3:def 8,WAYBEL_3:28;
          end;
         hence h >= g by WAYBEL_3:28;
        end;
       then f >= g by A1,YELLOW_0:31;
      hence f.i >= x by A6,WAYBEL_3:28;
     end;
    hence ex_inf_of pi(X, i), J.i by A3,YELLOW_0:31;
   end;
   assume for i being Element of I holds ex_inf_of pi(X,i), J.i;
   then consider f being Element of product J such that
      for i being Element of I holds f.i = inf pi(X,i) and
A8: f is_<=_than X and
A9: for g being Element of product J st X is_>=_than g holds f >= g by Lm2;
   thus ex_inf_of X, product J by A8,A9,YELLOW_0:31;
  end;

theorem Th35:
 for I being non empty set
 for J being Poset-yielding non-Empty ManySortedSet of I
 for X being Subset of product J
  st ex_sup_of X, product J
  for i being Element of I holds (sup X).i = sup pi(X,i)
  proof let I be non empty set;
   let J be Poset-yielding non-Empty ManySortedSet of I;
   let X be Subset of product J; assume ex_sup_of X, product J;
 then for i being Element of I holds ex_sup_of pi(X,i), J.i by Th33;
   then consider f being Element of product J such that
A1: for i being Element of I holds f.i = sup pi(X,i) and
A2: f is_>=_than X and
A3: for g being Element of product J st X is_<=_than g holds f <= g by Lm1;
      sup X = f by A2,A3,YELLOW_0:30;
   hence thesis by A1;
  end;

theorem Th36:
 for I being non empty set
 for J being Poset-yielding non-Empty ManySortedSet of I
 for X being Subset of product J
  st ex_inf_of X, product J
  for i being Element of I holds (inf X).i = inf pi(X,i)
  proof let I be non empty set;
   let J be Poset-yielding non-Empty ManySortedSet of I;
   let X be Subset of product J; assume ex_inf_of X, product J;
 then for i being Element of I holds ex_inf_of pi(X,i), J.i by Th34;
   then consider f being Element of product J such that
A1: for i being Element of I holds f.i = inf pi(X,i) and
A2: f is_<=_than X and
A3: for g being Element of product J st X is_>=_than g holds f >= g by Lm2;
      inf X = f by A2,A3,YELLOW_0:31;
   hence thesis by A1;
  end;

theorem Th37:
 for I being non empty set
 for J being RelStr-yielding non-Empty reflexive-yielding ManySortedSet of I
 for X being directed Subset of product J
 for i being Element of I holds pi(X,i) is directed
  proof let I be non empty set;
   let J be RelStr-yielding non-Empty reflexive-yielding ManySortedSet of I;
   let X be directed Subset of product J;
   let i be Element of I; let x,y be Element of J.i;
   assume x in pi(X,i);
   then consider f being Function such that
A1:  f in X & x = f.i by CARD_3:def 6;
   assume y in pi(X,i);
   then consider g being Function such that
A2:  g in X & y = g.i by CARD_3:def 6;
   reconsider f,g as Element of product J by A1,A2;
   consider h being Element of product J such that
A3:  h in X & f <= h & g <= h by A1,A2,WAYBEL_0:def 1;
   take h.i;
   thus h.i in pi(X,i) by A3,CARD_3:def 6;
   thus thesis by A1,A2,A3,WAYBEL_3:28;
  end;

theorem Th38:
 for I being non empty set
 for J,K being RelStr-yielding non-Empty ManySortedSet of I
  st for i being Element of I holds K.i is SubRelStr of J.i
 holds product K is SubRelStr of product J
  proof let I be non empty set;
   let J,K be RelStr-yielding non-Empty ManySortedSet of I such that
A1:  for i being Element of I holds K.i is SubRelStr of J.i;
A2:  the carrier of product K = product Carrier K by YELLOW_1:def 4;
A3:  the carrier of product J = product Carrier J by YELLOW_1:def 4;
A4:  dom Carrier J = I & dom Carrier K = I by PBOOLE:def 3;
      now let i be set; assume i in I; then reconsider j = i as Element of I;
A5:    (ex R being 1-sorted st R = J.j & (Carrier J).j = the carrier of R) &
      (ex R being 1-sorted st R = K.j & (Carrier K).j = the carrier of R)
       by PRALG_1:def 13;
        K.j is SubRelStr of J.j by A1;
     hence (Carrier K).i c= (Carrier J).i by A5,YELLOW_0:def 13;
    end;
   hence
A6:  the carrier of product K c= the carrier of product J
     by A2,A3,A4,CARD_3:38;
   let x,y be set; assume
A7:  [x,y] in the InternalRel of product K;
then A8:  x in the carrier of product K & y in the carrier of product K
     by ZFMISC_1:106;
   then reconsider x,y as Element of product K;
   reconsider f = x, g = y as Element of product J by A6,A8;
A9:  x <= y by A7,ORDERS_1:def 9;
      now let i be Element of I;
        K.i is SubRelStr of J.i & x.i <= y.i by A1,A9,WAYBEL_3:28;
     hence f.i <= g.i by YELLOW_0:60;
    end;
    then f <= g by WAYBEL_3:28;
   hence thesis by ORDERS_1:def 9;
  end;

theorem Th39:
 for I being non empty set
 for J,K being RelStr-yielding non-Empty ManySortedSet of I
  st for i being Element of I holds K.i is full SubRelStr of J.i
 holds product K is full SubRelStr of product J
  proof let I be non empty set;
   let J,K be RelStr-yielding non-Empty ManySortedSet of I; assume
A1:  for i being Element of I holds K.i is full SubRelStr of J.i;
    then for i being Element of I holds K.i is SubRelStr of J.i;
   then reconsider S = product K as non empty SubRelStr of product J by Th38;
A2:  (the InternalRel of product J)|_2 the carrier of S =
      (the InternalRel of product J)/\[:the carrier of S,the carrier of S:]
       by WELLORD1:def 6;
      S is full
     proof
         the InternalRel of S c= the InternalRel of product J
        by YELLOW_0:def 13;
      hence the InternalRel of S c= (the InternalRel of product J)|_2
         the carrier of S by A2,XBOOLE_1:19;
      let x,y be set; assume
         [x,y] in (the InternalRel of product J)|_2 the carrier of S;
then A3:     [x,y] in the InternalRel of product J &
       [x,y] in [:the carrier of S, the carrier of S:] by A2,XBOOLE_0:def 3
;
       then x in the carrier of S & y in the carrier of S by ZFMISC_1:106;
      then reconsider x, y as Element of S;
      reconsider a = x, b = y as Element of product J by YELLOW_0:59;
      reconsider x, y as Element of product K;
A4:     a <= b by A3,ORDERS_1:def 9;
         now let i be Element of I;
           a.i <= b.i & K.i is full SubRelStr of J.i & x.i in the carrier of K.
i
          by A1,A4,WAYBEL_3:28;
        hence x.i <= y.i by YELLOW_0:61;
       end;
       then x <= y by WAYBEL_3:28;
      hence thesis by ORDERS_1:def 9;
     end;
   hence thesis;
  end;

theorem
   for L being non empty RelStr, S being non empty SubRelStr of L, X being set
  holds S|^X is SubRelStr of L|^X
   proof let L be non empty RelStr, S be non empty SubRelStr of L, X be set;
A1:   S|^X = product (X --> S) & L|^X = product (X --> L) by YELLOW_1:def 5;
    per cases; suppose X = {};
      then S|^X = RelStr (#{{}}, id {{}}#) & L|^X = RelStr (#{{}},
id {
{}}#)
       by YELLOW_1:27;
     hence thesis by YELLOW_6:15;
    suppose X <> {};
     then reconsider X as non empty set;
        now let i be Element of X;
          (X --> L).i = L & (X --> S).i = S by FUNCOP_1:13;
       hence (X --> S).i is SubRelStr of (X --> L).i;
      end;
     hence thesis by A1,Th38;
   end;

theorem Th41:
 for L being non empty RelStr, S be full non empty SubRelStr of L, X be set
  holds S|^X is full SubRelStr of L|^X
   proof let L be non empty RelStr, S be full non empty SubRelStr of L,
     X be set;
A1:   S|^X = product (X --> S) & L|^X = product (X --> L) by YELLOW_1:def 5;
    per cases; suppose X = {};
      then S|^X = RelStr (#{{}}, id {{}}#) & L|^X = RelStr (#{{}},id {{}}#)
       by YELLOW_1:27;
     hence thesis by YELLOW_6:15;
    suppose X <> {};
     then reconsider X as non empty set;
        now let i be Element of X;
          (X --> L).i = L & (X --> S).i = S by FUNCOP_1:13;
       hence (X --> S).i is full SubRelStr of (X --> L).i;
      end;
     hence thesis by A1,Th39;
   end;

begin :: Inheritance

definition
 let S,T be non empty RelStr, X be set;
 pred S inherits_sup_of X,T means:Def6:
  ex_sup_of X,T implies "\/"(X, T) in the carrier of S;

 pred S inherits_inf_of X,T means:Def7:
  ex_inf_of X,T implies "/\"(X, T) in the carrier of S;
end;

theorem Th42:
 for T being non empty transitive RelStr
 for S being full non empty SubRelStr of T
 for X being Subset of S
  holds S inherits_sup_of X,T iff
    (ex_sup_of X,T implies ex_sup_of X, S & sup X = "\/"(X, T))
  proof let T be non empty transitive RelStr;
   let S be full non empty SubRelStr of T;
   let X be Subset of S;
   hereby assume that
A1:   S inherits_sup_of X,T and
A2:   ex_sup_of X,T;
      "\/"(X, T) in the carrier of S by A1,A2,Def6;
    hence ex_sup_of X, S & sup X = "\/"(X, T) by A2,YELLOW_0:65;
   end;
   assume
A3:  ex_sup_of X,T implies ex_sup_of X, S & sup X = "\/"(X, T);
   assume ex_sup_of X,T; hence thesis by A3;
  end;

theorem
   for T being non empty transitive RelStr
 for S being full non empty SubRelStr of T
 for X being Subset of S
  holds S inherits_inf_of X,T iff
    (ex_inf_of X,T implies ex_inf_of X, S & inf X = "/\"(X, T))
  proof let T be non empty transitive RelStr;
   let S be full non empty SubRelStr of T;
   let X be Subset of S;
   hereby assume that
A1:   S inherits_inf_of X,T and
A2:   ex_inf_of X,T;
      "/\"(X, T) in the carrier of S by A1,A2,Def7;
    hence ex_inf_of X, S & inf X = "/\"(X, T) by A2,YELLOW_0:64;
   end;
   assume
A3:  ex_inf_of X,T implies ex_inf_of X, S & inf X = "/\"(X, T);
   assume ex_inf_of X,T; hence thesis by A3;
  end;

scheme ProductSupsInheriting
 { I() -> non empty set,
   J,K() -> Poset-yielding non-Empty ManySortedSet of I(),
   P[set, set] }:
  for X being Subset of product K() st P[X, product K()]
   holds product K() inherits_sup_of X, product J()
 provided
A1:   for X being Subset of product K() st P[X, product K()]
    for i being Element of I() holds P[pi(X, i), K().i]
 and
A2:   for i being Element of I() holds K().i is full SubRelStr of J().i
 and
A3:   for i being Element of I(), X being Subset of K().i st P[X, K().i]
    holds K().i inherits_sup_of X, J().i
  proof let X be Subset of product K() such that
A4:  P[X, product K()] and
A5:  ex_sup_of X, product J();
   set f = "\/"(X, product J());
      product K() is SubRelStr of product J() by A2,Th39;
    then the carrier of product K() c= the carrier of product J()
     by YELLOW_0:def 13;
    then X c= the carrier of product J() by XBOOLE_1:1;
   then reconsider Y = X as Subset of product J();
A6:  dom f = I() by WAYBEL_3:27;
      now let i be Element of I();
        P[pi(X, i), K().i] by A1,A4;
then A7:    K().i inherits_sup_of pi(X, i), J().i by A3;
        ex_sup_of pi(Y,i), J().i by A5,Th33;
      then sup pi(Y,i) in the carrier of K().i by A7,Def6;
      then f.i in the carrier of K().i by A5,Th35;
     hence f.i is Element of K().i;
    end;
    then "\/"(X, product J()) is Element of product K() by A6,WAYBEL_3:27;
   hence thesis;
  end;

scheme PowerSupsInheriting
 { I() -> non empty set,
   L() -> non empty Poset,
   S() -> non empty full SubRelStr of L(),
   P[set, set] }:
  for X being Subset of S()|^I() st P[X, S()|^I()]
   holds S()|^I() inherits_sup_of X, L()|^I()
 provided
A1:   for X being Subset of S()|^I() st P[X, S()|^I()]
    for i being Element of I() holds P[pi(X, i), S()]
 and
A2:   for X being Subset of S() st P[X, S()] holds S() inherits_sup_of X, L()
  proof
   defpred p[set,set] means P[$1,$2];
   reconsider K = I() --> S(), J = I() --> L() as
     Poset-yielding non-Empty ManySortedSet of I();
A3:  S()|^I() = product K & L()|^I() = product J by YELLOW_1:def 5;
A4: now let X be Subset of product K such that
A5:   p[X, product K];
     let i be Element of I();
        K.i = S() by FUNCOP_1:13;
     hence p[pi(X, i), K.i] by A1,A3,A5;
    end;
A6: now let i be Element of I();
        K.i = S() & J.i = L() by FUNCOP_1:13;
     hence K.i is full SubRelStr of J.i;
    end;
A7: now let i be Element of I(), X be Subset of K.i such that
A8:   p[X, K.i];
        K.i = S() & J.i = L() by FUNCOP_1:13;
     hence K.i inherits_sup_of X, J.i by A2,A8;
    end;
      for X being Subset of product K st p[X, product K]
     holds product K inherits_sup_of X, product J
      from ProductSupsInheriting(A4,A6,A7);
   hence thesis by A3;
  end;

scheme ProductInfsInheriting
 { I() -> non empty set,
   J,K() -> Poset-yielding non-Empty ManySortedSet of I(),
   P[set, set] }:
  for X being Subset of product K() st P[X, product K()]
   holds product K() inherits_inf_of X, product J()
 provided
A1:   for X being Subset of product K() st P[X, product K()]
    for i being Element of I() holds P[pi(X, i), K().i]
 and
A2:   for i being Element of I() holds K().i is full SubRelStr of J().i
 and
A3:   for i being Element of I(), X being Subset of K().i st P[X, K().i]
    holds K().i inherits_inf_of X, J().i
  proof let X be Subset of product K() such that
A4:  P[X, product K()] and
A5:  ex_inf_of X, product J();
   set f = "/\"(X, product J());
      product K() is SubRelStr of product J() by A2,Th39;
    then the carrier of product K() c= the carrier of product J()
     by YELLOW_0:def 13;
    then X c= the carrier of product J() by XBOOLE_1:1;
   then reconsider Y = X as Subset of product J();
A6:  dom f = I() by WAYBEL_3:27;
      now let i be Element of I();
        P[pi(X, i), K().i] by A1,A4;
then A7:    K().i inherits_inf_of pi(X, i), J().i by A3;
        ex_inf_of pi(Y,i), J().i by A5,Th34;
      then inf pi(Y,i) in the carrier of K().i by A7,Def7;
      then f.i in the carrier of K().i by A5,Th36;
     hence f.i is Element of K().i;
    end;
    then "/\"(X, product J()) is Element of product K() by A6,WAYBEL_3:27;
   hence thesis;
  end;

scheme PowerInfsInheriting
 { I() -> non empty set,
   L() -> non empty Poset,
   S() -> non empty full SubRelStr of L(),
   P[set, set] }:
  for X being Subset of S()|^I() st P[X, S()|^I()]
   holds S()|^I() inherits_inf_of X, L()|^I()
 provided
A1:   for X being Subset of S()|^I() st P[X, S()|^I()]
    for i being Element of I() holds P[pi(X, i), S()]
 and
A2:   for X being Subset of S() st P[X, S()] holds S() inherits_inf_of X, L()
  proof
   defpred p[set,set] means P[$1,$2];
   reconsider K = I() --> S(), J = I() --> L() as
     Poset-yielding non-Empty ManySortedSet of I();
A3:  S()|^I() = product K & L()|^I() = product J by YELLOW_1:def 5;
A4: now let X be Subset of product K such that
A5:   p[X, product K];
     let i be Element of I();
        K.i = S() by FUNCOP_1:13;
     hence p[pi(X, i), K.i] by A1,A3,A5;
    end;
A6: now let i be Element of I();
        K.i = S() & J.i = L() by FUNCOP_1:13;
     hence K.i is full SubRelStr of J.i;
    end;
A7: now let i be Element of I(), X be Subset of K.i such that
A8:   p[X, K.i];
        K.i = S() & J.i = L() by FUNCOP_1:13;
     hence K.i inherits_inf_of X, J.i by A2,A8;
    end;
      for X being Subset of product K st p[X, product K]
     holds product K inherits_inf_of X, product J
      from ProductInfsInheriting(A4,A6,A7);
   hence thesis by A3;
  end;

definition
 let I be set;
 let L be non empty RelStr;
 let X be non empty Subset of L|^I;
 let i be set;
 cluster pi(X,i) -> non empty;
 coherence
  proof L|^I = product (I --> L) by YELLOW_1:def 5;
   then reconsider Y = X as non empty Subset of product (I --> L);
   consider f being Element of Y;
   f in the carrier of product (I --> L); then
   f in product Carrier (I --> L) by YELLOW_1:def 4; then
   reconsider f as Function by AMI_1:22;
   f.i in pi(X,i) by CARD_3:def 6;
   hence thesis;
  end;
end;

theorem
   for L being non empty Poset
 for S being directed-sups-inheriting non empty full SubRelStr of L
 for X be non empty set
  holds S|^X is directed-sups-inheriting SubRelStr of L|^X
  proof let L be non empty Poset;
   let S be directed-sups-inheriting non empty full SubRelStr of L;
   let X be non empty set;
   reconsider SX = S|^X as full non empty SubRelStr of L|^X by Th41;
   defpred P[set, non empty reflexive RelStr] means
     $1 is directed non empty Subset of $2;
A1: now let A be Subset of S|^X; assume P[A,S|^X];
     then reconsider B = A as directed non empty Subset of S|^X;
     let i be Element of X;
        product (X --> S) = S|^X & (X --> S).i = S
       by FUNCOP_1:13,YELLOW_1:def 5;
      then pi(B, i) is directed non empty Subset of S by Th37;
     hence P[pi(A, i),S];
    end;
A2: now let X be Subset of S; assume P[X,S];
      then
      ex_sup_of X,L implies ex_sup_of X, S & sup X = "\/"(X, L) by WAYBEL_0:7;
     hence S inherits_sup_of X, L by Th42;
    end;
      SX is directed-sups-inheriting
     proof let A be directed Subset of SX;
         for A being Subset of S|^X st P[A,S|^X]
        holds S|^X inherits_sup_of A, L|^X
         from PowerSupsInheriting(A1,A2);
       then A <> {} implies S|^X inherits_sup_of A, L|^X;
      hence thesis by Def6;
     end;
   hence thesis;
  end;

definition
 let I be non empty set;
 let J be RelStr-yielding non-Empty ManySortedSet of I;
 let X be non empty Subset of product J;
 let i be set;
 cluster pi(X,i) -> non empty;
 coherence
  proof consider f being Element of X;
   f in the carrier of product J; then
   f in product Carrier J by YELLOW_1:def 4; then
   reconsider f as Function by AMI_1:22;
   f.i in pi(X,i) by CARD_3:def 6;
   hence thesis;
  end;
end;

theorem Th45:
 for X being non empty set
 for L being up-complete (non empty Poset)
  holds L|^X is up-complete
  proof let X be non empty set;
   let L be up-complete (non empty Poset);
A1:  L|^X = product (X --> L) by YELLOW_1:def 5;
      now let A be non empty directed Subset of L|^X;
     reconsider B = A as non empty directed Subset of product (X --> L) by A1;
        now let x be Element of X;
A2:      (X --> L).x = L by FUNCOP_1:13;
          pi(B,x) is directed non empty by Th37;
       hence ex_sup_of pi(A,x), (X --> L).x by A2,WAYBEL_0:75;
      end;
     hence ex_sup_of A,L|^X by A1,Th33;
    end;
   hence thesis by WAYBEL_0:75;
  end;

definition
 let L be up-complete (non empty Poset);
 let X be non empty set;
 cluster L|^X -> up-complete;
 coherence by Th45;
end;

begin :: Topological retracts

definition
 let T be TopSpace;
 cluster the topology of T -> non empty;
 coherence by PRE_TOPC:def 1;
end;

theorem Th46:
 for T being non empty TopSpace, S being non empty SubSpace of T
 for f being ::continuous
 map of T,S st f is_a_retraction
  holds rng f = the carrier of S
  proof let T be non empty TopSpace, S be non empty SubSpace of T;
   let f be map of T,S such that
A1:  for W being Point of T st W in the carrier of S holds f.W=W;
   thus rng f c= the carrier of S;
      [#]T = the carrier of T & [#]S = the carrier of S by PRE_TOPC:12;
then A2:  the carrier of S c= the carrier of T by PRE_TOPC:def 9;
   let x be set; assume
A3:  x in the carrier of S;
    then x in the carrier of T by A2;
    then f.x = x & x in dom f by A1,A3,FUNCT_2:def 1;
   hence thesis by FUNCT_1:def 5;
  end;

theorem
   for T being non empty TopSpace, S being non empty SubSpace of T
 for f being continuous map of T,S st f is_a_retraction
  holds f is idempotent
  proof let T be non empty TopSpace, S be non empty SubSpace of T;
   let f be continuous map of T,S such that
A1:  f is_a_retraction;
      [#]T = the carrier of T & [#]S = the carrier of S by PRE_TOPC:12;
then A2:  the carrier of S c= the carrier of T by PRE_TOPC:def 9;
A3:  dom f = the carrier of T & rng f = the carrier of S
     by A1,Th46,FUNCT_2:def 1;
then A4:  dom (f*f) = the carrier of T by A2,RELAT_1:46;
      now let x be set; assume x in the carrier of T;
     then (f*f).x = f.(f.x) & f.x in rng f by A3,FUNCT_1:23,def 5;
     hence (f*f).x = f.x by A1,A2,A3,BORSUK_1:def 19;
    end;
    then f*f = f by A3,A4,FUNCT_1:9;
   hence thesis by QUANTAL1:def 9;
  end;

theorem Th48:
 for T being non empty TopSpace, V being open Subset of T
  holds chi(V, the carrier of T) is continuous map of T, Sierpinski_Space
  proof let T be non empty TopSpace, V be open Subset of T;
    the carrier of Sierpinski_Space = {0,1} by WAYBEL18:def 9;
   then reconsider c = chi(V, the carrier of T) as map of T, Sierpinski_Space;
      c = chi(c"{1}, the carrier of T) by FUNCT_3:49;
then A1:  V = c"{1} by FUNCT_3:47;
A2:  c"{} = {}T by RELAT_1:171;
A3:  c"{0,1} = the carrier of T by FUNCT_2:48 .= [#]T by PRE_TOPC:12;
      now let W be Subset of Sierpinski_Space;
     assume W is open;
      then W in the topology of Sierpinski_Space by PRE_TOPC:def 5;
      then W in {{}, {1}, {0,1}} by WAYBEL18:def 9;
     hence c"W is open by A1,A2,A3,ENUMSET1:13;
    end;
   hence thesis by TOPS_2:55;
  end;

theorem
   for T being non empty TopSpace, x,y being Element of T
  st for W being open Subset of T st y in W holds x in W
  holds (0,1) --> (y,x) is continuous map of Sierpinski_Space, T
  proof let T be non empty TopSpace;
   let x,y be Element of T such that
A1:  for W being open Subset of T st y in W holds x in W;
A2:  the carrier of Sierpinski_Space = {0,1} by WAYBEL18:def 9;
   then reconsider i = (0,1) --> (y,x) as map of Sierpinski_Space, T;
A3:  i.0 = y & i.1 = x by FUNCT_4:66;
A4:  0 in {0,1} & 1 in {0,1} & 0 in {0} & not 1 in {0} by TARSKI:def 1,def 2;
      now let W be Subset of T; assume
      W is open;
      then A5: y in W & x in W or not y in W & x in W or not y in W & not x in
 W by A1;
        i"W = {} or i"W = {0} or i"W = {1} or i"W = {0,1} by A2,ZFMISC_1:42;
      then i"W in {{}, {1}, {0,1}} by A3,A4,A5,ENUMSET1:14,FUNCT_2:46;
      then i"W in the topology of Sierpinski_Space by WAYBEL18:def 9;
     hence i"W is open by PRE_TOPC:def 5;
    end;
   hence thesis by TOPS_2:55;
  end;

theorem
   for T being non empty TopSpace, x,y being Element of T
 for V being open Subset of T
  st x in V & not y in V
  holds chi(V, the carrier of T)*((0,1) --> (y,x)) = id Sierpinski_Space
  proof let T be non empty TopSpace;
   let x,y be Element of T, V be open Subset of T such that
A1:  x in V & not y in V;
A2:  the carrier of Sierpinski_Space = {0,1} by WAYBEL18:def 9;
   then reconsider i = (0,1) --> (y,x) as map of Sierpinski_Space, T;
   reconsider c = chi(V, the carrier of T) as map of T, Sierpinski_Space
     by Th48;
A3:  i.0 = y & i.1 = x by FUNCT_4:66;
A4:  c.x = 1 & c.y = 0 by A1,FUNCT_3:def 3;
      now
     thus c*i is map of Sierpinski_Space, Sierpinski_Space;
     let a be Element of Sierpinski_Space;
        a = 0 or a = 1 by A2,TARSKI:def 2;
     hence (c*i).a = a by A3,A4,FUNCT_2:21
        .= (id Sierpinski_Space).a by GRCAT_1:11;
    end;
   hence thesis by YELLOW_2:9;
  end;

theorem
   for T being non empty 1-sorted, V,W being Subset of T
 for S being TopAugmentation of BoolePoset 1
 for f, g being map of T, S
  st f = chi(V, the carrier of T) & g = chi(W, the carrier of T)
  holds V c= W iff f <= g
  proof let T be non empty 1-sorted, V,W be Subset of T;
   let S be TopAugmentation of BoolePoset 1;
A1:  the RelStr of S = BoolePoset 1 by YELLOW_9:def 4;
   let c1, c2 be map of T, S such that
A2:  c1 = chi(V, the carrier of T) & c2 = chi(W, the carrier of T);
   hereby assume
A3:   V c= W;
       now let z be set; assume z in the carrier of T;
      then reconsider x = z as Element of T;
      reconsider a = c1.x, b = c2.x as Element of BoolePoset 1
        by A1;
         x in V & x in W or not x in V by A3;
       then c1.x = 1 & c2.x = 1 or c1.x = 0 by A2,FUNCT_3:def 3;
       then c1.x c= c2.x by XBOOLE_1:2;
       then a <= b by YELLOW_1:2;
       then c1.x <= c2.x by A1,YELLOW_0:1;
      hence ex a,b being Element of S st a = c1.z & b = c2.z & a <= b;
     end;
    hence c1 <= c2 by YELLOW_2:def 1;
   end;
   assume A4: c1 <= c2;
   let x be set; assume
A5:  x in V & not x in W;
   then reconsider x as Element of T;
   reconsider a = c1.x, b = c2.x as Element of BoolePoset 1
     by A1;
      ex a,b being Element of S st a = c1.x & b = c2.x & a <= b by A4,YELLOW_2:
def 1;
    then c1.x = 1 & c2.x = 0 & a <= b by A1,A2,A5,FUNCT_3:def 3,YELLOW_0:1;
    then 1 c= 0 & 0 c= 1 & 0 <> 1 by XBOOLE_1:2,YELLOW_1:2;
   hence thesis by XBOOLE_0:def 10;
  end;

theorem
   for L being non empty RelStr, X being non empty set
 for R being full non empty SubRelStr of L|^X
  st for a being set holds a is Element of R iff
       ex x being Element of L st a = X --> x
  holds L, R are_isomorphic
  proof let L be non empty RelStr, X be non empty set;
   let R be full non empty SubRelStr of L|^X such that
A1:  for a being set holds a is Element of R iff
       ex x being Element of L st a = X --> x;
   deffunc F(set) = X --> $1;
   consider f being ManySortedSet of the carrier of L such that
A2:  for i being Element of L holds f.i = F(i) from LambdaDMS;
A3:  dom f = the carrier of L by PBOOLE:def 3;
    rng f c= the carrier of R
     proof let y be set; assume y in rng f;
      then consider x being set such that
A4:    x in dom f & y = f.x by FUNCT_1:def 5;
      reconsider x as Element of L by A3,A4;
         y = X --> x by A2,A4;
       then y is Element of R by A1;
      hence thesis;
     end;
    then f is Function of the carrier of L, the carrier of R by A3,FUNCT_2:4;
   then reconsider f as map of L, R;
   take f;
A5:  rng f = the carrier of R
     proof thus rng f c= the carrier of R;
      let x be set; assume x in the carrier of R;
      then reconsider a = x as Element of R;
      consider i being Element of L such that
A6:    a = X --> i by A1;
         a = f.i by A2,A6;
      hence thesis by A3,FUNCT_1:def 5;
     end;
A7:  f is one-to-one
     proof let x,y be Element of L;
         f.x = X --> x & f.y = X --> y by A2;
       then f.x = [:X,{x}:] & f.y = [:X,{y}:] by FUNCOP_1:def 2;
       then f.x = f.y implies {x} = {y} by ZFMISC_1:134;
      hence thesis by ZFMISC_1:6;
     end;
      now let x,y be Element of L;
A8:   f.x = X --> x & f.y = X --> y by A2;
     reconsider a = f.x, b = f.y as Element of L|^X by YELLOW_0:59;
     hereby assume
A9:    x <= y;
         X --> x <= X --> y
        proof let i be set; assume i in X;
          then (X --> x).i = x & (X --> y).i = y by FUNCOP_1:13;
         hence ex p,q being Element of L st
            p = (X --> x).i & q = (X --> y).i & p <= q by A9;
        end;
       then a <= b & f.x in the carrier of R by A8,WAYBEL10:12;
      hence f.x <= f.y by YELLOW_0:61;
     end;
A10:   L|^X = product (X --> L) by YELLOW_1:def 5;
     reconsider a' = a, b' = b as Element of product (X --> L) by YELLOW_1:def
5;
     consider i being Element of X;
A11:   (X --> L).i = L by FUNCOP_1:13;
     assume f.x <= f.y;
      then a <= b by YELLOW_0:60;
      then a'.i <= b'.i by A10,WAYBEL_3:28;
      then x <= (X --> y).i by A8,A11,FUNCOP_1:13;
     hence x <= y by FUNCOP_1:13;
    end;
   hence f is isomorphic by A5,A7,WAYBEL_0:66;
  end;


theorem
   for S,T being non empty TopSpace holds
   S, T are_homeomorphic iff
    ex f being continuous map of S,T, g being continuous map of T,S
      st f*g = id T & g*f = id S
  proof let S,T be non empty TopSpace;
A1:  id T = id the carrier of T & id S = id the carrier of S by GRCAT_1:def 11;
A2:  [#]T = the carrier of T & [#]S = the carrier of S by PRE_TOPC:12;
   hereby assume S, T are_homeomorphic;
    then consider f being map of S,T such that
A3:   f is_homeomorphism by T_0TOPSP:def 1;
    reconsider f as continuous map of S,T by A3,TOPS_2:def 5;
    reconsider g = f" as continuous map of T,S by A3,TOPS_2:def 5;
    take f,g;
       f is one-to-one & rng f = [#]T & dom f = [#]S by A3,TOPS_2:def 5;
    hence f*g = id T & g*f = id S by A1,A2,TOPS_2:65;
   end;
   given f being continuous map of S,T, g being continuous map of T,S such that
A4:  f*g = id T & g*f = id S;
   take f;
A5:  f is one-to-one & rng f = [#]T & dom f = [#]S by A1,A2,A4,FUNCT_2:29,def 1
;
    then g = f qua Function" by A1,A2,A4,FUNCT_2:36
     .= f" by A5,TOPS_2:def 4;
   hence f is_homeomorphism by A5,TOPS_2:def 5;
  end;

theorem Th54:
 for T, S, R being non empty TopSpace
 for f being map of T,S, g being map of S,T, h being map of S, R
   st f*g = id S & h is_homeomorphism
   holds (h*f)*(g*(h")) = id R
  proof let T, S, R be non empty TopSpace;
   let f be map of T,S, g be map of S,T, h be map of S, R such that
A1:  f*g = id S and
A2:  h is_homeomorphism;
A3:  h is one-to-one & rng h = [#]R & dom h = [#]S by A2,TOPS_2:def 5;
   thus (h*f)*(g*(h")) = (h*f)*g*(h") by RELAT_1:55
     .= h*(f*g)*(h") by RELAT_1:55
     .= h*(id the carrier of S)*(h") by A1,GRCAT_1:def 11
     .= h*(h") by FUNCT_2:23
     .= id rng h by A3,TOPS_2:65
     .= id the carrier of R by A3,PRE_TOPC:12
     .= id R by GRCAT_1:def 11;
  end;

theorem Th55:
 for T, S, R being non empty TopSpace
   st S is_Retract_of T & S, R are_homeomorphic
   holds R is_Retract_of T
  proof let T, S, R be non empty TopSpace;
   given f being continuous map of S,T, g being continuous map of T,S such that
A1:  g*f = id S;
   given h being map of S,R such that
A2:  h is_homeomorphism;
A3:  h is continuous & h" is continuous by A2,TOPS_2:def 5;
   then reconsider f' = f*(h") as continuous map of R,T by TOPS_2:58;
   reconsider g' = h*g as continuous map of T,R by A3,TOPS_2:58;
   take f',g'; thus thesis by A1,A2,Th54;
  end;

theorem Th56:
 for T being non empty TopSpace, S being non empty SubSpace of T
  holds incl(S,T) is continuous
  proof let T be non empty TopSpace, S be non empty SubSpace of T;
    the carrier of S c= the carrier of T by BORSUK_1:35;
    then incl(S,T) = id the carrier of S by YELLOW_9:def 1
     .= id S by GRCAT_1:def 11;
   hence thesis by TOPMETR:7;
  end;

theorem Th57:
 for T being non empty TopSpace
 for S being non empty SubSpace of T, f being continuous map of T,S
   st f is_a_retraction
   holds f*incl(S,T) = id S
  proof let T be non empty TopSpace, S be non empty SubSpace of T;
   let f be continuous map of T,S such that
A1:  f is_a_retraction;
      [#]T = the carrier of T & [#]S = the carrier of S by PRE_TOPC:12;
then A2:  the carrier of S c= the carrier of T by PRE_TOPC:def 9;
then A3:  incl(S,T) = id the carrier of S by YELLOW_9:def 1;
      now let x be Element of S;
      x in the carrier of S;
     then reconsider y = x as Point of T by A2;
     thus (f*incl(S,T)).x = f.((incl(S,T)).x) by FUNCT_2:21
       .= f.x by A3,FUNCT_1:35 .= y by A1,BORSUK_1:def 19
       .= (id S).x by GRCAT_1:11;
    end;
   hence thesis by YELLOW_2:9;
  end;

theorem Th58:
 for T being non empty TopSpace, S being non empty SubSpace of T
   st S is_a_retract_of T
   holds S is_Retract_of T
  proof let T be non empty TopSpace, S be non empty SubSpace of T;
   given f be continuous map of T,S such that
A1:  f is_a_retraction;
   reconsider g = incl(S,T) as continuous map of S,T by Th56;
   take g,f; thus thesis by A1,Th57;
  end;

theorem
   for R,T being non empty TopSpace holds
   R is_Retract_of T iff
    ex S being non empty SubSpace of T
     st S is_a_retract_of T & S,R are_homeomorphic
  proof let R,T be non empty TopSpace;
   hereby assume R is_Retract_of T;
    then consider f being map of T,T such that
A1:   f is continuous & f*f = f & Image f, R are_homeomorphic
      by WAYBEL18:def 8;
    reconsider S = Image f as non empty SubSpace of T;
    take S; f = corestr f by WAYBEL18:def 7;
    then reconsider f as continuous map of T,S by A1,WAYBEL18:11;
       [#]S = the carrier of S & [#]T = the carrier of T by PRE_TOPC:12;
     then the carrier of S c= the carrier of T by PRE_TOPC:def 9;
     then rng f c= the carrier of T by XBOOLE_1:1;
    then reconsider rf = rng f as Subset of T;
       now let x be Point of T; assume x in the carrier of S;
       then x in the carrier of T|rf by WAYBEL18:def 6;
       then x in [#](T|rf) by PRE_TOPC:12;
       then x in rng f by PRE_TOPC:def 10;
       then ex y being set st y in dom f & x = f.y by FUNCT_1:def 5;
      hence f.x = x by A1,FUNCT_1:23;
     end;
     then f is_a_retraction by BORSUK_1:def 19;
    hence S is_a_retract_of T & S, R are_homeomorphic by A1,BORSUK_1:def 20;
   end;
   given S being non empty SubSpace of T such that
A2:  S is_a_retract_of T & S,R are_homeomorphic;
      S is_Retract_of T by A2,Th58;
   hence R is_Retract_of T by A2,Th55;
  end;


Back to top