:: YELLOW14 semantic presentation begin theorem :: YELLOW14:1 bool 1 = {0,1} by CARD_1:49, ZFMISC_1:24; theorem Th2: :: YELLOW14:2 for X being set for Y being Subset of X holds rng ((id X) | Y) = Y proof let X be set ; ::_thesis: for Y being Subset of X holds rng ((id X) | Y) = Y let Y be Subset of X; ::_thesis: rng ((id X) | Y) = Y set f = id X; A1: (id X) | Y is Function of Y,X by FUNCT_2:32; hereby :: according to TARSKI:def_3,XBOOLE_0:def_10 ::_thesis: Y c= rng ((id X) | Y) let y be set ; ::_thesis: ( y in rng ((id X) | Y) implies y in Y ) assume y in rng ((id X) | Y) ; ::_thesis: y in Y then consider x being set such that A2: x in dom ((id X) | Y) and A3: y = ((id X) | Y) . x by FUNCT_1:def_3; ((id X) | Y) . x = (id X) . x by A2, FUNCT_1:47 .= x by A2, FUNCT_1:17 ; hence y in Y by A1, A2, A3, FUNCT_2:def_1; ::_thesis: verum end; let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in Y or y in rng ((id X) | Y) ) ( X = {} implies Y = {} ) ; then A4: dom ((id X) | Y) = Y by A1, FUNCT_2:def_1; assume A5: y in Y ; ::_thesis: y in rng ((id X) | Y) then ((id X) | Y) . y = (id X) . y by FUNCT_1:49 .= y by A5, FUNCT_1:18 ; hence y in rng ((id X) | Y) by A4, A5, FUNCT_1:def_3; ::_thesis: verum end; theorem :: YELLOW14:3 for S being empty 1-sorted for T being 1-sorted for f being Function of S,T st rng f = [#] T holds T is empty ; theorem :: YELLOW14:4 for S being 1-sorted for T being empty 1-sorted for f being Function of S,T st dom f = [#] S holds S is empty ; theorem :: YELLOW14:5 for S being non empty 1-sorted for T being 1-sorted for f being Function of S,T st dom f = [#] S holds not T is empty ; theorem :: YELLOW14:6 for S being 1-sorted for T being non empty 1-sorted for f being Function of S,T st rng f = [#] T holds not S is empty ; definition let S be non empty reflexive RelStr ; let T be non empty RelStr ; let f be Function of S,T; redefine attr f is directed-sups-preserving means :: YELLOW14:def 1 for X being non empty directed Subset of S holds f preserves_sup_of X; compatibility ( f is directed-sups-preserving iff for X being non empty directed Subset of S holds f preserves_sup_of X ) proof thus ( f is directed-sups-preserving implies for X being non empty directed Subset of S holds f preserves_sup_of X ) by WAYBEL_0:def_37; ::_thesis: ( ( for X being non empty directed Subset of S holds f preserves_sup_of X ) implies f is directed-sups-preserving ) assume A1: for X being non empty directed Subset of S holds f preserves_sup_of X ; ::_thesis: f is directed-sups-preserving let X be Subset of S; :: according to WAYBEL_0:def_37 ::_thesis: ( X is empty or not X is directed or f preserves_sup_of X ) thus ( X is empty or not X is directed or f preserves_sup_of X ) by A1; ::_thesis: verum end; end; :: deftheorem defines directed-sups-preserving YELLOW14:def_1_:_ for S being non empty reflexive RelStr for T being non empty RelStr for f being Function of S,T holds ( f is directed-sups-preserving iff for X being non empty directed Subset of S holds f preserves_sup_of X ); definition let R be 1-sorted ; let N be NetStr over R; attrN is Function-yielding means :Def2: :: YELLOW14:def 2 the mapping of N is Function-yielding ; end; :: deftheorem Def2 defines Function-yielding YELLOW14:def_2_:_ for R being 1-sorted for N being NetStr over R holds ( N is Function-yielding iff the mapping of N is Function-yielding ); registration cluster non empty constituted-Functions for 1-sorted ; existence ex b1 being 1-sorted st ( not b1 is empty & b1 is constituted-Functions ) proof take A = 1-sorted(# {{}} #); ::_thesis: ( not A is empty & A is constituted-Functions ) thus not the carrier of A is empty ; :: according to STRUCT_0:def_1 ::_thesis: A is constituted-Functions let a be Element of A; :: according to MONOID_0:def_1 ::_thesis: a is set thus a is set ; ::_thesis: verum end; end; registration cluster non empty strict constituted-Functions for RelStr ; existence ex b1 being RelStr st ( b1 is strict & not b1 is empty & b1 is constituted-Functions ) proof take A = RelStr(# {{}},(id {{}}) #); ::_thesis: ( A is strict & not A is empty & A is constituted-Functions ) thus ( A is strict & not A is empty ) ; ::_thesis: A is constituted-Functions let a be Element of A; :: according to MONOID_0:def_1 ::_thesis: a is set thus a is set ; ::_thesis: verum end; end; registration let R be constituted-Functions 1-sorted ; cluster -> Function-yielding for NetStr over R; coherence for b1 being NetStr over R holds b1 is Function-yielding proof let N be NetStr over R; ::_thesis: N is Function-yielding let x be set ; :: according to FUNCOP_1:def_6,YELLOW14:def_2 ::_thesis: ( not x in dom the mapping of N or the mapping of N . x is set ) assume x in dom the mapping of N ; ::_thesis: the mapping of N . x is set then the mapping of N . x in rng the mapping of N by FUNCT_1:def_3; hence the mapping of N . x is set ; ::_thesis: verum end; end; registration let R be constituted-Functions 1-sorted ; cluster strict Function-yielding for NetStr over R; existence ex b1 being NetStr over R st ( b1 is strict & b1 is Function-yielding ) proof take A = NetStr(# the carrier of R,(id the carrier of R),(id the carrier of R) #); ::_thesis: ( A is strict & A is Function-yielding ) thus A is strict ; ::_thesis: A is Function-yielding let x be set ; :: according to FUNCOP_1:def_6,YELLOW14:def_2 ::_thesis: ( not x in dom the mapping of A or the mapping of A . x is set ) assume x in dom the mapping of A ; ::_thesis: the mapping of A . x is set hence the mapping of A . x is set by FUNCT_1:18; ::_thesis: verum end; end; registration let R be non empty constituted-Functions 1-sorted ; cluster non empty strict Function-yielding for NetStr over R; existence ex b1 being NetStr over R st ( b1 is strict & not b1 is empty & b1 is Function-yielding ) proof take A = NetStr(# the carrier of R,(id the carrier of R),(id the carrier of R) #); ::_thesis: ( A is strict & not A is empty & A is Function-yielding ) thus ( A is strict & not A is empty ) ; ::_thesis: A is Function-yielding let x be set ; :: according to FUNCOP_1:def_6,YELLOW14:def_2 ::_thesis: ( not x in dom the mapping of A or the mapping of A . x is set ) assume x in dom the mapping of A ; ::_thesis: the mapping of A . x is set hence the mapping of A . x is set by FUNCT_1:18; ::_thesis: verum end; end; registration let R be constituted-Functions 1-sorted ; let N be Function-yielding NetStr over R; cluster the mapping of N -> Function-yielding ; coherence the mapping of N is Function-yielding by Def2; end; registration let R be non empty constituted-Functions 1-sorted ; cluster non empty transitive strict directed Function-yielding for NetStr over R; existence ex b1 being net of R st ( b1 is strict & b1 is Function-yielding ) proof set p = the Element of R; set N = the net of R; take ConstantNet ( the net of R, the Element of R) ; ::_thesis: ( ConstantNet ( the net of R, the Element of R) is strict & ConstantNet ( the net of R, the Element of R) is Function-yielding ) thus ( ConstantNet ( the net of R, the Element of R) is strict & ConstantNet ( the net of R, the Element of R) is Function-yielding ) ; ::_thesis: verum end; end; registration let S be non empty 1-sorted ; let N be non empty NetStr over S; cluster rng the mapping of N -> non empty ; coherence not rng the mapping of N is empty ; end; registration let S be non empty 1-sorted ; let N be non empty NetStr over S; cluster rng (netmap (N,S)) -> non empty ; coherence not rng (netmap (N,S)) is empty ; end; theorem :: YELLOW14:7 for A, B, C being non empty RelStr for f being Function of B,C for g, h being Function of A,B st g <= h & f is monotone holds f * g <= f * h proof let A, B, C be non empty RelStr ; ::_thesis: for f being Function of B,C for g, h being Function of A,B st g <= h & f is monotone holds f * g <= f * h let f be Function of B,C; ::_thesis: for g, h being Function of A,B st g <= h & f is monotone holds f * g <= f * h let g, h be Function of A,B; ::_thesis: ( g <= h & f is monotone implies f * g <= f * h ) assume that A1: g <= h and A2: for x, y being Element of B st x <= y holds f . x <= f . y ; :: according to WAYBEL_1:def_2 ::_thesis: f * g <= f * h for x being Element of A holds (f * g) . x <= (f * h) . x proof let x be Element of A; ::_thesis: (f * g) . x <= (f * h) . x A3: ( (f * g) . x = f . (g . x) & (f * h) . x = f . (h . x) ) by FUNCT_2:15; g . x <= h . x by A1, YELLOW_2:9; hence (f * g) . x <= (f * h) . x by A2, A3; ::_thesis: verum end; hence f * g <= f * h by YELLOW_2:9; ::_thesis: verum end; theorem :: YELLOW14:8 for S being non empty TopSpace for T being non empty TopSpace-like TopRelStr for f, g being Function of S,T for x, y being Element of (ContMaps (S,T)) st x = f & y = g holds ( x <= y iff f <= g ) proof let S be non empty TopSpace; ::_thesis: for T being non empty TopSpace-like TopRelStr for f, g being Function of S,T for x, y being Element of (ContMaps (S,T)) st x = f & y = g holds ( x <= y iff f <= g ) let T be non empty TopSpace-like TopRelStr ; ::_thesis: for f, g being Function of S,T for x, y being Element of (ContMaps (S,T)) st x = f & y = g holds ( x <= y iff f <= g ) let f, g be Function of S,T; ::_thesis: for x, y being Element of (ContMaps (S,T)) st x = f & y = g holds ( x <= y iff f <= g ) let x, y be Element of (ContMaps (S,T)); ::_thesis: ( x = f & y = g implies ( x <= y iff f <= g ) ) assume A1: ( x = f & y = g ) ; ::_thesis: ( x <= y iff f <= g ) A2: ContMaps (S,T) is full SubRelStr of T |^ the carrier of S by WAYBEL24:def_3; then reconsider x1 = x, y1 = y as Element of (T |^ the carrier of S) by YELLOW_0:58; hereby ::_thesis: ( f <= g implies x <= y ) assume x <= y ; ::_thesis: f <= g then x1 <= y1 by A2, YELLOW_0:59; hence f <= g by A1, WAYBEL10:11; ::_thesis: verum end; assume f <= g ; ::_thesis: x <= y then x1 <= y1 by A1, WAYBEL10:11; hence x <= y by A2, YELLOW_0:60; ::_thesis: verum end; definition let I be non empty set ; let R be non empty RelStr ; let f be Element of (R |^ I); let i be Element of I; :: original: . redefine funcf . i -> Element of R; coherence f . i is Element of R proof reconsider g = f as Element of (product (I --> R)) by YELLOW_1:def_5; g . i is Element of ((I --> R) . i) ; hence f . i is Element of R by FUNCOP_1:7; ::_thesis: verum end; end; begin theorem Th9: :: YELLOW14:9 for S, T being RelStr for f being Function of S,T st f is isomorphic holds f is onto proof let S, T be RelStr ; ::_thesis: for f being Function of S,T st f is isomorphic holds f is onto let f be Function of S,T; ::_thesis: ( f is isomorphic implies f is onto ) assume A1: f is isomorphic ; ::_thesis: f is onto percases ( ( not S is empty & not T is empty ) or S is empty or T is empty ) ; suppose ( not S is empty & not T is empty ) ; ::_thesis: f is onto hence rng f = the carrier of T by A1, WAYBEL_0:66; :: according to FUNCT_2:def_3 ::_thesis: verum end; suppose ( S is empty or T is empty ) ; ::_thesis: f is onto then T is empty by A1, WAYBEL_0:def_38; then the carrier of T = {} ; hence rng f = the carrier of T ; :: according to FUNCT_2:def_3 ::_thesis: verum end; end; end; registration let S, T be RelStr ; cluster Function-like quasi_total isomorphic -> onto for Element of K6(K7( the carrier of S, the carrier of T)); coherence for b1 being Function of S,T st b1 is isomorphic holds b1 is onto by Th9; end; theorem Th10: :: YELLOW14:10 for S, T being non empty RelStr for f being Function of S,T st f is isomorphic holds f /" is isomorphic proof let S, T be non empty RelStr ; ::_thesis: for f being Function of S,T st f is isomorphic holds f /" is isomorphic let f be Function of S,T; ::_thesis: ( f is isomorphic implies f /" is isomorphic ) assume A1: f is isomorphic ; ::_thesis: f /" is isomorphic then ( ex g being Function of T,S st ( g = f " & g is monotone ) & rng f = the carrier of T ) by WAYBEL_0:66, WAYBEL_0:def_38; hence f /" is isomorphic by A1, TOPS_2:def_4, WAYBEL_0:68; ::_thesis: verum end; theorem :: YELLOW14:11 for S, T being non empty RelStr st S,T are_isomorphic & S is with_infima holds T is with_infima proof let S, T be non empty RelStr ; ::_thesis: ( S,T are_isomorphic & S is with_infima implies T is with_infima ) given f being Function of S,T such that A1: f is isomorphic ; :: according to WAYBEL_1:def_8 ::_thesis: ( not S is with_infima or T is with_infima ) assume A2: for a, b being Element of S ex c being Element of S st ( c <= a & c <= b & ( for c9 being Element of S st c9 <= a & c9 <= b holds c9 <= c ) ) ; :: according to LATTICE3:def_11 ::_thesis: T is with_infima let x, y be Element of T; :: according to LATTICE3:def_11 ::_thesis: ex b1 being Element of the carrier of T st ( b1 <= x & b1 <= y & ( for b2 being Element of the carrier of T holds ( not b2 <= x or not b2 <= y or b2 <= b1 ) ) ) consider c being Element of S such that A3: ( c <= (f /") . x & c <= (f /") . y ) and A4: for c9 being Element of S st c9 <= (f /") . x & c9 <= (f /") . y holds c9 <= c by A2; take f . c ; ::_thesis: ( f . c <= x & f . c <= y & ( for b1 being Element of the carrier of T holds ( not b1 <= x or not b1 <= y or b1 <= f . c ) ) ) A5: ex g being Function of T,S st ( g = f " & g is monotone ) by A1, WAYBEL_0:def_38; A6: rng f = the carrier of T by A1, WAYBEL_0:66; A7: f /" = f " by A1, TOPS_2:def_4; ( f . c <= f . ((f /") . x) & f . c <= f . ((f /") . y) ) by A1, A3, WAYBEL_0:66; hence ( f . c <= x & f . c <= y ) by A1, A6, A7, FUNCT_1:35; ::_thesis: for b1 being Element of the carrier of T holds ( not b1 <= x or not b1 <= y or b1 <= f . c ) let z9 be Element of T; ::_thesis: ( not z9 <= x or not z9 <= y or z9 <= f . c ) assume ( z9 <= x & z9 <= y ) ; ::_thesis: z9 <= f . c then ( (f /") . z9 <= (f /") . x & (f /") . z9 <= (f /") . y ) by A7, A5, WAYBEL_1:def_2; then (f /") . z9 <= c by A4; then f . ((f /") . z9) <= f . c by A1, WAYBEL_0:66; hence z9 <= f . c by A1, A6, A7, FUNCT_1:35; ::_thesis: verum end; theorem :: YELLOW14:12 for S, T being non empty RelStr st S,T are_isomorphic & S is with_suprema holds T is with_suprema proof let S, T be non empty RelStr ; ::_thesis: ( S,T are_isomorphic & S is with_suprema implies T is with_suprema ) given f being Function of S,T such that A1: f is isomorphic ; :: according to WAYBEL_1:def_8 ::_thesis: ( not S is with_suprema or T is with_suprema ) assume A2: for a, b being Element of S ex c being Element of S st ( a <= c & b <= c & ( for c9 being Element of S st a <= c9 & b <= c9 holds c <= c9 ) ) ; :: according to LATTICE3:def_10 ::_thesis: T is with_suprema let x, y be Element of T; :: according to LATTICE3:def_10 ::_thesis: ex b1 being Element of the carrier of T st ( x <= b1 & y <= b1 & ( for b2 being Element of the carrier of T holds ( not x <= b2 or not y <= b2 or b1 <= b2 ) ) ) consider c being Element of S such that A3: ( (f /") . x <= c & (f /") . y <= c ) and A4: for c9 being Element of S st (f /") . x <= c9 & (f /") . y <= c9 holds c <= c9 by A2; take f . c ; ::_thesis: ( x <= f . c & y <= f . c & ( for b1 being Element of the carrier of T holds ( not x <= b1 or not y <= b1 or f . c <= b1 ) ) ) A5: ex g being Function of T,S st ( g = f " & g is monotone ) by A1, WAYBEL_0:def_38; A6: rng f = the carrier of T by A1, WAYBEL_0:66; A7: f /" = f " by A1, TOPS_2:def_4; ( f . ((f /") . x) <= f . c & f . ((f /") . y) <= f . c ) by A1, A3, WAYBEL_0:66; hence ( x <= f . c & y <= f . c ) by A1, A6, A7, FUNCT_1:35; ::_thesis: for b1 being Element of the carrier of T holds ( not x <= b1 or not y <= b1 or f . c <= b1 ) let z9 be Element of T; ::_thesis: ( not x <= z9 or not y <= z9 or f . c <= z9 ) assume ( x <= z9 & y <= z9 ) ; ::_thesis: f . c <= z9 then ( (f /") . x <= (f /") . z9 & (f /") . y <= (f /") . z9 ) by A7, A5, WAYBEL_1:def_2; then c <= (f /") . z9 by A4; then f . c <= f . ((f /") . z9) by A1, WAYBEL_0:66; hence f . c <= z9 by A1, A6, A7, FUNCT_1:35; ::_thesis: verum end; theorem Th13: :: YELLOW14:13 for L being RelStr st L is empty holds L is bounded proof let L be RelStr ; ::_thesis: ( L is empty implies L is bounded ) assume A1: L is empty ; ::_thesis: L is bounded set x = the Element of L; thus L is lower-bounded :: according to YELLOW_0:def_6 ::_thesis: L is upper-bounded proof take the Element of L ; :: according to YELLOW_0:def_4 ::_thesis: the Element of L is_<=_than the carrier of L let a be Element of L; :: according to LATTICE3:def_8 ::_thesis: ( not a in the carrier of L or the Element of L <= a ) assume a in the carrier of L ; ::_thesis: the Element of L <= a hence the Element of L <= a by A1; ::_thesis: verum end; take the Element of L ; :: according to YELLOW_0:def_5 ::_thesis: the carrier of L is_<=_than the Element of L let a be Element of L; :: according to LATTICE3:def_9 ::_thesis: ( not a in the carrier of L or a <= the Element of L ) assume a in the carrier of L ; ::_thesis: a <= the Element of L hence a <= the Element of L by A1; ::_thesis: verum end; registration cluster empty -> bounded for RelStr ; coherence for b1 being RelStr st b1 is empty holds b1 is bounded by Th13; end; theorem :: YELLOW14:14 for S, T being RelStr st S,T are_isomorphic & S is lower-bounded holds T is lower-bounded proof let S, T be RelStr ; ::_thesis: ( S,T are_isomorphic & S is lower-bounded implies T is lower-bounded ) given f being Function of S,T such that A1: f is isomorphic ; :: according to WAYBEL_1:def_8 ::_thesis: ( not S is lower-bounded or T is lower-bounded ) percases ( ( not S is empty & not T is empty ) or S is empty or T is empty ) ; suppose ( not S is empty & not T is empty ) ; ::_thesis: ( not S is lower-bounded or T is lower-bounded ) then reconsider s = S, t = T as non empty RelStr ; given X being Element of S such that A2: X is_<=_than the carrier of S ; :: according to YELLOW_0:def_4 ::_thesis: T is lower-bounded reconsider x = X as Element of s ; reconsider g = f as Function of s,t ; reconsider y = g . x as Element of T ; take y ; :: according to YELLOW_0:def_4 ::_thesis: y is_<=_than the carrier of T y is_<=_than g .: ([#] S) by A1, A2, YELLOW_2:13; then y is_<=_than rng g by RELSET_1:22; hence y is_<=_than the carrier of T by A1, WAYBEL_0:66; ::_thesis: verum end; suppose ( S is empty or T is empty ) ; ::_thesis: ( not S is lower-bounded or T is lower-bounded ) then T is empty by A1, WAYBEL_0:def_38; then reconsider T = T as bounded RelStr ; T is lower-bounded ; hence ( not S is lower-bounded or T is lower-bounded ) ; ::_thesis: verum end; end; end; theorem :: YELLOW14:15 for S, T being RelStr st S,T are_isomorphic & S is upper-bounded holds T is upper-bounded proof let S, T be RelStr ; ::_thesis: ( S,T are_isomorphic & S is upper-bounded implies T is upper-bounded ) given f being Function of S,T such that A1: f is isomorphic ; :: according to WAYBEL_1:def_8 ::_thesis: ( not S is upper-bounded or T is upper-bounded ) percases ( ( not S is empty & not T is empty ) or S is empty or T is empty ) ; suppose ( not S is empty & not T is empty ) ; ::_thesis: ( not S is upper-bounded or T is upper-bounded ) then reconsider s = S, t = T as non empty RelStr ; given X being Element of S such that A2: X is_>=_than the carrier of S ; :: according to YELLOW_0:def_5 ::_thesis: T is upper-bounded reconsider x = X as Element of s ; reconsider g = f as Function of s,t ; reconsider y = g . x as Element of T ; take y ; :: according to YELLOW_0:def_5 ::_thesis: the carrier of T is_<=_than y y is_>=_than g .: ([#] S) by A1, A2, YELLOW_2:14; then y is_>=_than rng g by RELSET_1:22; hence the carrier of T is_<=_than y by A1, WAYBEL_0:66; ::_thesis: verum end; suppose ( S is empty or T is empty ) ; ::_thesis: ( not S is upper-bounded or T is upper-bounded ) then T is empty by A1, WAYBEL_0:def_38; then reconsider T = T as bounded RelStr ; T is lower-bounded ; hence ( not S is upper-bounded or T is upper-bounded ) ; ::_thesis: verum end; end; end; theorem :: YELLOW14:16 for S, T being non empty RelStr for A being Subset of S for f being Function of S,T st f is isomorphic & ex_sup_of A,S holds ex_sup_of f .: A,T proof let S, T be non empty RelStr ; ::_thesis: for A being Subset of S for f being Function of S,T st f is isomorphic & ex_sup_of A,S holds ex_sup_of f .: A,T let A be Subset of S; ::_thesis: for f being Function of S,T st f is isomorphic & ex_sup_of A,S holds ex_sup_of f .: A,T let f be Function of S,T; ::_thesis: ( f is isomorphic & ex_sup_of A,S implies ex_sup_of f .: A,T ) assume A1: f is isomorphic ; ::_thesis: ( not ex_sup_of A,S or ex_sup_of f .: A,T ) A2: f " (f .: A) c= A by A1, FUNCT_1:82; A3: rng f = [#] T by A1, WAYBEL_0:66; A4: f /" = f " by A1, TOPS_2:def_4; given a being Element of S such that A5: A is_<=_than a and A6: for b being Element of S st A is_<=_than b holds b >= a and A7: for c being Element of S st A is_<=_than c & ( for b being Element of S st A is_<=_than b holds b >= c ) holds c = a ; :: according to YELLOW_0:def_7 ::_thesis: ex_sup_of f .: A,T take f . a ; :: according to YELLOW_0:def_7 ::_thesis: ( f .: A is_<=_than f . a & ( for b1 being Element of the carrier of T holds ( not f .: A is_<=_than b1 or f . a <= b1 ) ) & ( for b1 being Element of the carrier of T holds ( not f .: A is_<=_than b1 or ex b2 being Element of the carrier of T st ( f .: A is_<=_than b2 & not b1 <= b2 ) or b1 = f . a ) ) ) thus f .: A is_<=_than f . a by A1, A5, WAYBEL13:19; ::_thesis: ( ( for b1 being Element of the carrier of T holds ( not f .: A is_<=_than b1 or f . a <= b1 ) ) & ( for b1 being Element of the carrier of T holds ( not f .: A is_<=_than b1 or ex b2 being Element of the carrier of T st ( f .: A is_<=_than b2 & not b1 <= b2 ) or b1 = f . a ) ) ) A8: f /" is isomorphic by A1, Th10; A9: dom f = the carrier of S by FUNCT_2:def_1; then A c= f " (f .: A) by FUNCT_1:76; then A10: f " (f .: A) = A by A2, XBOOLE_0:def_10; hereby ::_thesis: for b1 being Element of the carrier of T holds ( not f .: A is_<=_than b1 or ex b2 being Element of the carrier of T st ( f .: A is_<=_than b2 & not b1 <= b2 ) or b1 = f . a ) let b be Element of T; ::_thesis: ( f .: A is_<=_than b implies b >= f . a ) assume f .: A is_<=_than b ; ::_thesis: b >= f . a then (f /") .: (f .: A) is_<=_than (f /") . b by A8, WAYBEL13:19; then f " (f .: A) is_<=_than (f /") . b by A1, A3, TOPS_2:55; then (f /") . b >= a by A6, A10; then f . ((f /") . b) >= f . a by A1, WAYBEL_0:66; hence b >= f . a by A1, A3, A4, FUNCT_1:35; ::_thesis: verum end; let c be Element of T; ::_thesis: ( not f .: A is_<=_than c or ex b1 being Element of the carrier of T st ( f .: A is_<=_than b1 & not c <= b1 ) or c = f . a ) assume A11: f .: A is_<=_than c ; ::_thesis: ( ex b1 being Element of the carrier of T st ( f .: A is_<=_than b1 & not c <= b1 ) or c = f . a ) assume A12: for b being Element of T st f .: A is_<=_than b holds b >= c ; ::_thesis: c = f . a A13: for b being Element of S st A is_<=_than b holds b >= (f /") . c proof let b be Element of S; ::_thesis: ( A is_<=_than b implies b >= (f /") . c ) assume A is_<=_than b ; ::_thesis: b >= (f /") . c then f .: A is_<=_than f . b by A1, WAYBEL13:19; then f . b >= c by A12; then (f /") . (f . b) >= (f /") . c by A8, WAYBEL_0:66; hence b >= (f /") . c by A1, A4, A9, FUNCT_1:34; ::_thesis: verum end; (f /") .: (f .: A) is_<=_than (f /") . c by A8, A11, WAYBEL13:19; then A is_<=_than (f /") . c by A1, A3, A10, TOPS_2:55; then (f /") . c = a by A7, A13; hence c = f . a by A1, A3, A4, FUNCT_1:35; ::_thesis: verum end; theorem :: YELLOW14:17 for S, T being non empty RelStr for A being Subset of S for f being Function of S,T st f is isomorphic & ex_inf_of A,S holds ex_inf_of f .: A,T proof let S, T be non empty RelStr ; ::_thesis: for A being Subset of S for f being Function of S,T st f is isomorphic & ex_inf_of A,S holds ex_inf_of f .: A,T let A be Subset of S; ::_thesis: for f being Function of S,T st f is isomorphic & ex_inf_of A,S holds ex_inf_of f .: A,T let f be Function of S,T; ::_thesis: ( f is isomorphic & ex_inf_of A,S implies ex_inf_of f .: A,T ) assume A1: f is isomorphic ; ::_thesis: ( not ex_inf_of A,S or ex_inf_of f .: A,T ) A2: f " (f .: A) c= A by A1, FUNCT_1:82; A3: rng f = [#] T by A1, WAYBEL_0:66; A4: f /" = f " by A1, TOPS_2:def_4; given a being Element of S such that A5: A is_>=_than a and A6: for b being Element of S st A is_>=_than b holds b <= a and A7: for c being Element of S st A is_>=_than c & ( for b being Element of S st A is_>=_than b holds b <= c ) holds c = a ; :: according to YELLOW_0:def_8 ::_thesis: ex_inf_of f .: A,T take f . a ; :: according to YELLOW_0:def_8 ::_thesis: ( f . a is_<=_than f .: A & ( for b1 being Element of the carrier of T holds ( not b1 is_<=_than f .: A or b1 <= f . a ) ) & ( for b1 being Element of the carrier of T holds ( not b1 is_<=_than f .: A or ex b2 being Element of the carrier of T st ( b2 is_<=_than f .: A & not b2 <= b1 ) or b1 = f . a ) ) ) thus f .: A is_>=_than f . a by A1, A5, WAYBEL13:18; ::_thesis: ( ( for b1 being Element of the carrier of T holds ( not b1 is_<=_than f .: A or b1 <= f . a ) ) & ( for b1 being Element of the carrier of T holds ( not b1 is_<=_than f .: A or ex b2 being Element of the carrier of T st ( b2 is_<=_than f .: A & not b2 <= b1 ) or b1 = f . a ) ) ) A8: f /" is isomorphic by A1, Th10; A9: dom f = the carrier of S by FUNCT_2:def_1; then A c= f " (f .: A) by FUNCT_1:76; then A10: f " (f .: A) = A by A2, XBOOLE_0:def_10; hereby ::_thesis: for b1 being Element of the carrier of T holds ( not b1 is_<=_than f .: A or ex b2 being Element of the carrier of T st ( b2 is_<=_than f .: A & not b2 <= b1 ) or b1 = f . a ) let b be Element of T; ::_thesis: ( f .: A is_>=_than b implies b <= f . a ) assume f .: A is_>=_than b ; ::_thesis: b <= f . a then (f /") .: (f .: A) is_>=_than (f /") . b by A8, WAYBEL13:18; then f " (f .: A) is_>=_than (f /") . b by A1, A3, TOPS_2:55; then (f /") . b <= a by A6, A10; then f . ((f /") . b) <= f . a by A1, WAYBEL_0:66; hence b <= f . a by A1, A3, A4, FUNCT_1:35; ::_thesis: verum end; let c be Element of T; ::_thesis: ( not c is_<=_than f .: A or ex b1 being Element of the carrier of T st ( b1 is_<=_than f .: A & not b1 <= c ) or c = f . a ) assume A11: f .: A is_>=_than c ; ::_thesis: ( ex b1 being Element of the carrier of T st ( b1 is_<=_than f .: A & not b1 <= c ) or c = f . a ) assume A12: for b being Element of T st f .: A is_>=_than b holds b <= c ; ::_thesis: c = f . a A13: for b being Element of S st A is_>=_than b holds b <= (f /") . c proof let b be Element of S; ::_thesis: ( A is_>=_than b implies b <= (f /") . c ) assume A is_>=_than b ; ::_thesis: b <= (f /") . c then f .: A is_>=_than f . b by A1, WAYBEL13:18; then f . b <= c by A12; then (f /") . (f . b) <= (f /") . c by A8, WAYBEL_0:66; hence b <= (f /") . c by A1, A4, A9, FUNCT_1:34; ::_thesis: verum end; (f /") .: (f .: A) is_>=_than (f /") . c by A8, A11, WAYBEL13:18; then A is_>=_than (f /") . c by A1, A3, A10, TOPS_2:55; then (f /") . c = a by A7, A13; hence c = f . a by A1, A3, A4, FUNCT_1:35; ::_thesis: verum end; begin theorem :: YELLOW14:18 for S, T being TopStruct st ( S,T are_homeomorphic or ex f being Function of S,T st ( dom f = [#] S & rng f = [#] T ) ) holds ( S is empty iff T is empty ) proof let S, T be TopStruct ; ::_thesis: ( ( S,T are_homeomorphic or ex f being Function of S,T st ( dom f = [#] S & rng f = [#] T ) ) implies ( S is empty iff T is empty ) ) assume A1: ( S,T are_homeomorphic or ex f being Function of S,T st ( dom f = [#] S & rng f = [#] T ) ) ; ::_thesis: ( S is empty iff T is empty ) percases ( S,T are_homeomorphic or ex f being Function of S,T st ( dom f = [#] S & rng f = [#] T ) ) by A1; suppose S,T are_homeomorphic ; ::_thesis: ( S is empty iff T is empty ) then consider f being Function of S,T such that A2: f is being_homeomorphism by T_0TOPSP:def_1; ( rng f = [#] T & dom f = [#] S ) by A2, TOPS_2:def_5; hence ( S is empty iff T is empty ) ; ::_thesis: verum end; suppose ex f being Function of S,T st ( dom f = [#] S & rng f = [#] T ) ; ::_thesis: ( S is empty iff T is empty ) hence ( S is empty iff T is empty ) ; ::_thesis: verum end; end; end; theorem :: YELLOW14:19 for T being non empty TopSpace holds T, TopStruct(# the carrier of T, the topology of T #) are_homeomorphic proof let T be non empty TopSpace; ::_thesis: T, TopStruct(# the carrier of T, the topology of T #) are_homeomorphic reconsider f = id T as Function of T,TopStruct(# the carrier of T, the topology of T #) ; take f ; :: according to T_0TOPSP:def_1 ::_thesis: f is being_homeomorphism thus dom f = [#] T by FUNCT_2:def_1; :: according to TOPS_2:def_5 ::_thesis: ( rng f = [#] TopStruct(# the carrier of T, the topology of T #) & f is one-to-one & f is continuous & f /" is continuous ) thus rng f = [#] T by TOPS_2:def_5 .= [#] TopStruct(# the carrier of T, the topology of T #) ; ::_thesis: ( f is one-to-one & f is continuous & f /" is continuous ) thus f is V14() ; ::_thesis: ( f is continuous & f /" is continuous ) thus f is continuous by YELLOW12:36; ::_thesis: f /" is continuous thus f /" is continuous by YELLOW12:36; ::_thesis: verum end; registration let T be non empty reflexive Scott TopRelStr ; cluster open -> upper inaccessible for Element of K6( the carrier of T); coherence for b1 being Subset of T st b1 is open holds ( b1 is inaccessible & b1 is upper ) by WAYBEL11:def_4; cluster upper inaccessible -> open for Element of K6( the carrier of T); coherence for b1 being Subset of T st b1 is inaccessible & b1 is upper holds b1 is open by WAYBEL11:def_4; end; theorem :: YELLOW14:20 for T being TopStruct for x, y being Point of T for X, Y being Subset of T st X = {x} & Cl X c= Cl Y holds x in Cl Y proof let T be TopStruct ; ::_thesis: for x, y being Point of T for X, Y being Subset of T st X = {x} & Cl X c= Cl Y holds x in Cl Y let x, y be Point of T; ::_thesis: for X, Y being Subset of T st X = {x} & Cl X c= Cl Y holds x in Cl Y let X, Y be Subset of T; ::_thesis: ( X = {x} & Cl X c= Cl Y implies x in Cl Y ) assume that A1: X = {x} and A2: Cl X c= Cl Y ; ::_thesis: x in Cl Y X c= Cl X by PRE_TOPC:18; then A3: X c= Cl Y by A2, XBOOLE_1:1; x in X by A1, TARSKI:def_1; hence x in Cl Y by A3; ::_thesis: verum end; theorem :: YELLOW14:21 for T being TopStruct for x, y being Point of T for Y, V being Subset of T st Y = {y} & x in Cl Y & V is open & x in V holds y in V proof let T be TopStruct ; ::_thesis: for x, y being Point of T for Y, V being Subset of T st Y = {y} & x in Cl Y & V is open & x in V holds y in V let x, y be Point of T; ::_thesis: for Y, V being Subset of T st Y = {y} & x in Cl Y & V is open & x in V holds y in V let Y, V be Subset of T; ::_thesis: ( Y = {y} & x in Cl Y & V is open & x in V implies y in V ) assume A1: Y = {y} ; ::_thesis: ( not x in Cl Y or not V is open or not x in V or y in V ) assume ( x in Cl Y & V is open & x in V ) ; ::_thesis: y in V then Y meets V by PRE_TOPC:def_7; hence y in V by A1, ZFMISC_1:50; ::_thesis: verum end; theorem :: YELLOW14:22 for T being TopStruct for x, y being Point of T for X, Y being Subset of T st X = {x} & Y = {y} & ( for V being Subset of T st V is open & x in V holds y in V ) holds Cl X c= Cl Y proof let T be TopStruct ; ::_thesis: for x, y being Point of T for X, Y being Subset of T st X = {x} & Y = {y} & ( for V being Subset of T st V is open & x in V holds y in V ) holds Cl X c= Cl Y let x, y be Point of T; ::_thesis: for X, Y being Subset of T st X = {x} & Y = {y} & ( for V being Subset of T st V is open & x in V holds y in V ) holds Cl X c= Cl Y let X, Y be Subset of T; ::_thesis: ( X = {x} & Y = {y} & ( for V being Subset of T st V is open & x in V holds y in V ) implies Cl X c= Cl Y ) assume that A1: X = {x} and A2: ( Y = {y} & ( for V being Subset of T st V is open & x in V holds y in V ) ) ; ::_thesis: Cl X c= Cl Y let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in Cl X or z in Cl Y ) assume A3: z in Cl X ; ::_thesis: z in Cl Y for V being Subset of T st V is open & z in V holds Y meets V proof let V be Subset of T; ::_thesis: ( V is open & z in V implies Y meets V ) assume that A4: V is open and A5: z in V ; ::_thesis: Y meets V X meets V by A3, A4, A5, PRE_TOPC:def_7; then x in V by A1, ZFMISC_1:50; hence Y meets V by A2, A4, ZFMISC_1:48; ::_thesis: verum end; hence z in Cl Y by A3, PRE_TOPC:def_7; ::_thesis: verum end; theorem Th23: :: YELLOW14:23 for S, T being non empty TopSpace for A being irreducible Subset of S for B being Subset of T st A = B & TopStruct(# the carrier of S, the topology of S #) = TopStruct(# the carrier of T, the topology of T #) holds B is irreducible proof let S, T be non empty TopSpace; ::_thesis: for A being irreducible Subset of S for B being Subset of T st A = B & TopStruct(# the carrier of S, the topology of S #) = TopStruct(# the carrier of T, the topology of T #) holds B is irreducible let A be irreducible Subset of S; ::_thesis: for B being Subset of T st A = B & TopStruct(# the carrier of S, the topology of S #) = TopStruct(# the carrier of T, the topology of T #) holds B is irreducible let B be Subset of T; ::_thesis: ( A = B & TopStruct(# the carrier of S, the topology of S #) = TopStruct(# the carrier of T, the topology of T #) implies B is irreducible ) assume that A1: A = B and A2: TopStruct(# the carrier of S, the topology of S #) = TopStruct(# the carrier of T, the topology of T #) ; ::_thesis: B is irreducible ( not A is empty & A is closed ) by YELLOW_8:def_3; hence ( not B is empty & B is closed ) by A1, A2, TOPS_3:79; :: according to YELLOW_8:def_3 ::_thesis: for b1, b2 being Element of K6( the carrier of T) holds ( not b1 is closed or not b2 is closed or not B = K20(K6( the carrier of T),b1,b2) or b1 = B or b2 = B ) let B1, B2 be Subset of T; ::_thesis: ( not B1 is closed or not B2 is closed or not B = K20(K6( the carrier of T),B1,B2) or B1 = B or B2 = B ) assume that A3: ( B1 is closed & B2 is closed ) and A4: B = B1 \/ B2 ; ::_thesis: ( B1 = B or B2 = B ) reconsider A1 = B1, A2 = B2 as Subset of S by A2; ( A1 is closed & A2 is closed ) by A2, A3, TOPS_3:79; hence ( B1 = B or B2 = B ) by A1, A4, YELLOW_8:def_3; ::_thesis: verum end; theorem Th24: :: YELLOW14:24 for S, T being non empty TopSpace for a being Point of S for b being Point of T for A being Subset of S for B being Subset of T st a = b & A = B & TopStruct(# the carrier of S, the topology of S #) = TopStruct(# the carrier of T, the topology of T #) & a is_dense_point_of A holds b is_dense_point_of B proof let S, T be non empty TopSpace; ::_thesis: for a being Point of S for b being Point of T for A being Subset of S for B being Subset of T st a = b & A = B & TopStruct(# the carrier of S, the topology of S #) = TopStruct(# the carrier of T, the topology of T #) & a is_dense_point_of A holds b is_dense_point_of B let a be Point of S; ::_thesis: for b being Point of T for A being Subset of S for B being Subset of T st a = b & A = B & TopStruct(# the carrier of S, the topology of S #) = TopStruct(# the carrier of T, the topology of T #) & a is_dense_point_of A holds b is_dense_point_of B let b be Point of T; ::_thesis: for A being Subset of S for B being Subset of T st a = b & A = B & TopStruct(# the carrier of S, the topology of S #) = TopStruct(# the carrier of T, the topology of T #) & a is_dense_point_of A holds b is_dense_point_of B let A be Subset of S; ::_thesis: for B being Subset of T st a = b & A = B & TopStruct(# the carrier of S, the topology of S #) = TopStruct(# the carrier of T, the topology of T #) & a is_dense_point_of A holds b is_dense_point_of B let B be Subset of T; ::_thesis: ( a = b & A = B & TopStruct(# the carrier of S, the topology of S #) = TopStruct(# the carrier of T, the topology of T #) & a is_dense_point_of A implies b is_dense_point_of B ) assume ( a = b & A = B & TopStruct(# the carrier of S, the topology of S #) = TopStruct(# the carrier of T, the topology of T #) & a in A & A c= Cl {a} ) ; :: according to YELLOW_8:def_4 ::_thesis: b is_dense_point_of B hence ( b in B & B c= Cl {b} ) by TOPS_3:80; :: according to YELLOW_8:def_4 ::_thesis: verum end; theorem Th25: :: YELLOW14:25 for S, T being TopStruct for A being Subset of S for B being Subset of T st A = B & TopStruct(# the carrier of S, the topology of S #) = TopStruct(# the carrier of T, the topology of T #) & A is compact holds B is compact proof let S, T be TopStruct ; ::_thesis: for A being Subset of S for B being Subset of T st A = B & TopStruct(# the carrier of S, the topology of S #) = TopStruct(# the carrier of T, the topology of T #) & A is compact holds B is compact let A be Subset of S; ::_thesis: for B being Subset of T st A = B & TopStruct(# the carrier of S, the topology of S #) = TopStruct(# the carrier of T, the topology of T #) & A is compact holds B is compact let B be Subset of T; ::_thesis: ( A = B & TopStruct(# the carrier of S, the topology of S #) = TopStruct(# the carrier of T, the topology of T #) & A is compact implies B is compact ) assume that A1: A = B and A2: TopStruct(# the carrier of S, the topology of S #) = TopStruct(# the carrier of T, the topology of T #) and A3: for F being Subset-Family of S st F is Cover of A & F is open holds ex G being Subset-Family of S st ( G c= F & G is Cover of A & G is finite ) ; :: according to COMPTS_1:def_4 ::_thesis: B is compact let F be Subset-Family of T; :: according to COMPTS_1:def_4 ::_thesis: ( not F is Cover of B or not F is open or ex b1 being Element of K6(K6( the carrier of T)) st ( b1 c= F & b1 is Cover of B & b1 is finite ) ) assume A4: ( F is Cover of B & F is open ) ; ::_thesis: ex b1 being Element of K6(K6( the carrier of T)) st ( b1 c= F & b1 is Cover of B & b1 is finite ) reconsider K = F as Subset-Family of S by A2; consider L being Subset-Family of S such that A5: ( L c= K & L is Cover of A & L is finite ) by A1, A2, A3, A4, WAYBEL_9:19; reconsider G = L as Subset-Family of T by A2; take G ; ::_thesis: ( G c= F & G is Cover of B & G is finite ) thus ( G c= F & G is Cover of B & G is finite ) by A1, A5; ::_thesis: verum end; theorem :: YELLOW14:26 for S, T being non empty TopSpace st TopStruct(# the carrier of S, the topology of S #) = TopStruct(# the carrier of T, the topology of T #) & S is sober holds T is sober proof let S, T be non empty TopSpace; ::_thesis: ( TopStruct(# the carrier of S, the topology of S #) = TopStruct(# the carrier of T, the topology of T #) & S is sober implies T is sober ) assume that A1: TopStruct(# the carrier of S, the topology of S #) = TopStruct(# the carrier of T, the topology of T #) and A2: for A being irreducible Subset of S ex a being Point of S st ( a is_dense_point_of A & ( for b being Point of S st b is_dense_point_of A holds a = b ) ) ; :: according to YELLOW_8:def_5 ::_thesis: T is sober let B be irreducible Subset of T; :: according to YELLOW_8:def_5 ::_thesis: ex b1 being Element of the carrier of T st ( b1 is_dense_point_of B & ( for b2 being Element of the carrier of T holds ( not b2 is_dense_point_of B or b1 = b2 ) ) ) reconsider A = B as irreducible Subset of S by A1, Th23; consider a being Point of S such that A3: a is_dense_point_of A and A4: for b being Point of S st b is_dense_point_of A holds a = b by A2; reconsider p = a as Point of T by A1; take p ; ::_thesis: ( p is_dense_point_of B & ( for b1 being Element of the carrier of T holds ( not b1 is_dense_point_of B or p = b1 ) ) ) thus p is_dense_point_of B by A1, A3, Th24; ::_thesis: for b1 being Element of the carrier of T holds ( not b1 is_dense_point_of B or p = b1 ) let q be Point of T; ::_thesis: ( not q is_dense_point_of B or p = q ) reconsider b = q as Point of S by A1; assume q is_dense_point_of B ; ::_thesis: p = q then b is_dense_point_of A by A1, Th24; hence p = q by A4; ::_thesis: verum end; theorem :: YELLOW14:27 for S, T being non empty TopSpace st TopStruct(# the carrier of S, the topology of S #) = TopStruct(# the carrier of T, the topology of T #) & S is locally-compact holds T is locally-compact proof let S, T be non empty TopSpace; ::_thesis: ( TopStruct(# the carrier of S, the topology of S #) = TopStruct(# the carrier of T, the topology of T #) & S is locally-compact implies T is locally-compact ) assume that A1: TopStruct(# the carrier of S, the topology of S #) = TopStruct(# the carrier of T, the topology of T #) and A2: for x being Point of S for X being Subset of S st x in X & X is open holds ex Y being Subset of S st ( x in Int Y & Y c= X & Y is compact ) ; :: according to WAYBEL_3:def_9 ::_thesis: T is locally-compact let x be Point of T; :: according to WAYBEL_3:def_9 ::_thesis: for b1 being Element of K6( the carrier of T) holds ( not x in b1 or not b1 is open or ex b2 being Element of K6( the carrier of T) st ( x in Int b2 & b2 c= b1 & b2 is compact ) ) let X be Subset of T; ::_thesis: ( not x in X or not X is open or ex b1 being Element of K6( the carrier of T) st ( x in Int b1 & b1 c= X & b1 is compact ) ) assume A3: ( x in X & X is open ) ; ::_thesis: ex b1 being Element of K6( the carrier of T) st ( x in Int b1 & b1 c= X & b1 is compact ) reconsider A = X as Subset of S by A1; consider B being Subset of S such that A4: ( x in Int B & B c= A & B is compact ) by A1, A2, A3, TOPS_3:76; reconsider Y = B as Subset of T by A1; take Y ; ::_thesis: ( x in Int Y & Y c= X & Y is compact ) thus ( x in Int Y & Y c= X & Y is compact ) by A1, A4, Th25, TOPS_3:77; ::_thesis: verum end; theorem :: YELLOW14:28 for S, T being TopStruct st TopStruct(# the carrier of S, the topology of S #) = TopStruct(# the carrier of T, the topology of T #) & S is compact holds T is compact proof let S, T be TopStruct ; ::_thesis: ( TopStruct(# the carrier of S, the topology of S #) = TopStruct(# the carrier of T, the topology of T #) & S is compact implies T is compact ) assume that A1: TopStruct(# the carrier of S, the topology of S #) = TopStruct(# the carrier of T, the topology of T #) and A2: for F being Subset-Family of S st F is Cover of S & F is open holds ex G being Subset-Family of S st ( G c= F & G is Cover of S & G is finite ) ; :: according to COMPTS_1:def_1 ::_thesis: T is compact let F be Subset-Family of T; :: according to COMPTS_1:def_1 ::_thesis: ( not F is Cover of the carrier of T or not F is open or ex b1 being Element of K6(K6( the carrier of T)) st ( b1 c= F & b1 is Cover of the carrier of T & b1 is finite ) ) assume A3: ( F is Cover of T & F is open ) ; ::_thesis: ex b1 being Element of K6(K6( the carrier of T)) st ( b1 c= F & b1 is Cover of the carrier of T & b1 is finite ) reconsider K = F as Subset-Family of S by A1; consider L being Subset-Family of S such that A4: ( L c= K & L is Cover of S & L is finite ) by A1, A2, A3, WAYBEL_9:19; reconsider G = L as Subset-Family of T by A1; take G ; ::_thesis: ( G c= F & G is Cover of the carrier of T & G is finite ) thus ( G c= F & G is Cover of the carrier of T & G is finite ) by A1, A4; ::_thesis: verum end; definition let I be non empty set ; let T be non empty TopSpace; let x be Point of (product (I --> T)); let i be Element of I; :: original: . redefine funcx . i -> Element of T; coherence x . i is Element of T proof x . i is Point of T by FUNCOP_1:7; hence x . i is Element of T ; ::_thesis: verum end; end; theorem Th29: :: YELLOW14:29 for M being non empty set for J being non-Empty TopStruct-yielding ManySortedSet of M for x, y being Point of (product J) holds ( x in Cl {y} iff for i being Element of M holds x . i in Cl {(y . i)} ) proof let M be non empty set ; ::_thesis: for J being non-Empty TopStruct-yielding ManySortedSet of M for x, y being Point of (product J) holds ( x in Cl {y} iff for i being Element of M holds x . i in Cl {(y . i)} ) let J be non-Empty TopStruct-yielding ManySortedSet of M; ::_thesis: for x, y being Point of (product J) holds ( x in Cl {y} iff for i being Element of M holds x . i in Cl {(y . i)} ) let x, y be Point of (product J); ::_thesis: ( x in Cl {y} iff for i being Element of M holds x . i in Cl {(y . i)} ) hereby ::_thesis: ( ( for i being Element of M holds x . i in Cl {(y . i)} ) implies x in Cl {y} ) assume A1: x in Cl {y} ; ::_thesis: for i being Element of M holds x . i in Cl {(y . i)} let i be Element of M; ::_thesis: x . i in Cl {(y . i)} x in the carrier of (product J) ; then x in product (Carrier J) by WAYBEL18:def_3; then consider f being Function such that A2: x = f and A3: dom f = dom (Carrier J) and A4: for z being set st z in dom (Carrier J) holds f . z in (Carrier J) . z by CARD_3:def_5; A5: i in M ; for G being Subset of (J . i) st G is open & x . i in G holds {(y . i)} meets G proof let G be Subset of (J . i); ::_thesis: ( G is open & x . i in G implies {(y . i)} meets G ) assume that A6: G is open and A7: x . i in G ; ::_thesis: {(y . i)} meets G reconsider G9 = G as Subset of (J . i) ; ( [#] (J . i) <> {} & proj (J,i) is continuous ) by WAYBEL18:5; then A8: (proj (J,i)) " G9 is open by A6, TOPS_2:43; A9: for z being set st z in dom ((Carrier J) +* (i,G)) holds f . z in ((Carrier J) +* (i,G)) . z proof let z be set ; ::_thesis: ( z in dom ((Carrier J) +* (i,G)) implies f . z in ((Carrier J) +* (i,G)) . z ) assume z in dom ((Carrier J) +* (i,G)) ; ::_thesis: f . z in ((Carrier J) +* (i,G)) . z then A10: z in dom (Carrier J) by FUNCT_7:30; percases ( z = i or z <> i ) ; suppose z = i ; ::_thesis: f . z in ((Carrier J) +* (i,G)) . z hence f . z in ((Carrier J) +* (i,G)) . z by A2, A7, A10, FUNCT_7:31; ::_thesis: verum end; suppose z <> i ; ::_thesis: f . z in ((Carrier J) +* (i,G)) . z then ((Carrier J) +* (i,G)) . z = (Carrier J) . z by FUNCT_7:32; hence f . z in ((Carrier J) +* (i,G)) . z by A4, A10; ::_thesis: verum end; end; end; A11: product ((Carrier J) +* (i,G9)) = (proj (J,i)) " G9 by WAYBEL18:4; dom f = dom ((Carrier J) +* (i,G)) by A3, FUNCT_7:30; then x in product ((Carrier J) +* (i,G)) by A2, A9, CARD_3:def_5; then {y} meets (proj (J,i)) " G9 by A1, A8, A11, PRE_TOPC:def_7; then y in product ((Carrier J) +* (i,G)) by A11, ZFMISC_1:50; then consider g being Function such that A12: y = g and dom g = dom ((Carrier J) +* (i,G)) and A13: for z being set st z in dom ((Carrier J) +* (i,G)) holds g . z in ((Carrier J) +* (i,G)) . z by CARD_3:def_5; A14: i in dom (Carrier J) by A5, PARTFUN1:def_2; then i in dom ((Carrier J) +* (i,G)) by FUNCT_7:30; then g . i in ((Carrier J) +* (i,G)) . i by A13; then g . i in G by A14, FUNCT_7:31; hence {(y . i)} meets G by A12, ZFMISC_1:48; ::_thesis: verum end; hence x . i in Cl {(y . i)} by PRE_TOPC:def_7; ::_thesis: verum end; reconsider K = product_prebasis J as prebasis of (product J) by WAYBEL18:def_3; assume A15: for i being Element of M holds x . i in Cl {(y . i)} ; ::_thesis: x in Cl {y} for Z being finite Subset-Family of (product J) st Z c= K & x in Intersect Z holds Intersect Z meets {y} proof let Z be finite Subset-Family of (product J); ::_thesis: ( Z c= K & x in Intersect Z implies Intersect Z meets {y} ) assume that A16: Z c= K and A17: x in Intersect Z ; ::_thesis: Intersect Z meets {y} for Y being set st Y in Z holds y in Y proof let Y be set ; ::_thesis: ( Y in Z implies y in Y ) y in the carrier of (product J) ; then y in product (Carrier J) by WAYBEL18:def_3; then consider g being Function such that A18: y = g and A19: dom g = dom (Carrier J) and A20: for z being set st z in dom (Carrier J) holds g . z in (Carrier J) . z by CARD_3:def_5; assume A21: Y in Z ; ::_thesis: y in Y then Y in K by A16; then consider i being set , W being TopStruct , V being Subset of W such that A22: i in M and A23: V is open and A24: W = J . i and A25: Y = product ((Carrier J) +* (i,V)) by WAYBEL18:def_2; reconsider i = i as Element of M by A22; reconsider V = V as Subset of (J . i) by A24; x in Y by A17, A21, SETFAM_1:43; then A26: ex f being Function st ( x = f & dom f = dom ((Carrier J) +* (i,V)) & ( for z being set st z in dom ((Carrier J) +* (i,V)) holds f . z in ((Carrier J) +* (i,V)) . z ) ) by A25, CARD_3:def_5; x . i in Cl {(y . i)} by A15; then A27: ( x . i in V implies {(y . i)} meets V ) by A23, A24, PRE_TOPC:def_7; A28: for z being set st z in dom ((Carrier J) +* (i,V)) holds g . z in ((Carrier J) +* (i,V)) . z proof let z be set ; ::_thesis: ( z in dom ((Carrier J) +* (i,V)) implies g . z in ((Carrier J) +* (i,V)) . z ) assume A29: z in dom ((Carrier J) +* (i,V)) ; ::_thesis: g . z in ((Carrier J) +* (i,V)) . z then A30: z in dom (Carrier J) by FUNCT_7:30; percases ( z = i or z <> i ) ; supposeA31: z = i ; ::_thesis: g . z in ((Carrier J) +* (i,V)) . z then ((Carrier J) +* (i,V)) . z = V by A30, FUNCT_7:31; hence g . z in ((Carrier J) +* (i,V)) . z by A27, A26, A18, A29, A31, ZFMISC_1:50; ::_thesis: verum end; suppose z <> i ; ::_thesis: g . z in ((Carrier J) +* (i,V)) . z then ((Carrier J) +* (i,V)) . z = (Carrier J) . z by FUNCT_7:32; hence g . z in ((Carrier J) +* (i,V)) . z by A20, A30; ::_thesis: verum end; end; end; dom g = dom ((Carrier J) +* (i,V)) by A19, FUNCT_7:30; hence y in Y by A25, A18, A28, CARD_3:def_5; ::_thesis: verum end; then ( y in {y} & y in Intersect Z ) by SETFAM_1:43, TARSKI:def_1; hence Intersect Z meets {y} by XBOOLE_0:3; ::_thesis: verum end; hence x in Cl {y} by YELLOW_9:38; ::_thesis: verum end; theorem :: YELLOW14:30 for M being non empty set for T being non empty TopSpace for x, y being Point of (product (M --> T)) holds ( x in Cl {y} iff for i being Element of M holds x . i in Cl {(y . i)} ) proof let M be non empty set ; ::_thesis: for T being non empty TopSpace for x, y being Point of (product (M --> T)) holds ( x in Cl {y} iff for i being Element of M holds x . i in Cl {(y . i)} ) let T be non empty TopSpace; ::_thesis: for x, y being Point of (product (M --> T)) holds ( x in Cl {y} iff for i being Element of M holds x . i in Cl {(y . i)} ) let x, y be Point of (product (M --> T)); ::_thesis: ( x in Cl {y} iff for i being Element of M holds x . i in Cl {(y . i)} ) reconsider J = M --> T as non-Empty TopStruct-yielding ManySortedSet of M ; reconsider x9 = x, y9 = y as Point of (product J) ; thus ( x in Cl {y} implies for i being Element of M holds x . i in Cl {(y . i)} ) ::_thesis: ( ( for i being Element of M holds x . i in Cl {(y . i)} ) implies x in Cl {y} ) proof assume A1: x in Cl {y} ; ::_thesis: for i being Element of M holds x . i in Cl {(y . i)} let i be Element of M; ::_thesis: x . i in Cl {(y . i)} x9 . i in Cl {(y9 . i)} by A1, Th29; hence x . i in Cl {(y . i)} by FUNCOP_1:7; ::_thesis: verum end; assume A2: for i being Element of M holds x . i in Cl {(y . i)} ; ::_thesis: x in Cl {y} for i being Element of M holds x9 . i in Cl {(y9 . i)} proof let i be Element of M; ::_thesis: x9 . i in Cl {(y9 . i)} x . i in Cl {(y . i)} by A2; hence x9 . i in Cl {(y9 . i)} by FUNCOP_1:7; ::_thesis: verum end; hence x in Cl {y} by Th29; ::_thesis: verum end; theorem Th31: :: YELLOW14:31 for M being non empty set for i being Element of M for J being non-Empty TopStruct-yielding ManySortedSet of M for x being Point of (product J) holds pi ((Cl {x}),i) = Cl {(x . i)} proof let M be non empty set ; ::_thesis: for i being Element of M for J being non-Empty TopStruct-yielding ManySortedSet of M for x being Point of (product J) holds pi ((Cl {x}),i) = Cl {(x . i)} let i be Element of M; ::_thesis: for J being non-Empty TopStruct-yielding ManySortedSet of M for x being Point of (product J) holds pi ((Cl {x}),i) = Cl {(x . i)} let J be non-Empty TopStruct-yielding ManySortedSet of M; ::_thesis: for x being Point of (product J) holds pi ((Cl {x}),i) = Cl {(x . i)} let x be Point of (product J); ::_thesis: pi ((Cl {x}),i) = Cl {(x . i)} consider f being set such that A1: f in Cl {x} by XBOOLE_0:def_1; A2: f in the carrier of (product J) by A1; thus pi ((Cl {x}),i) c= Cl {(x . i)} :: according to XBOOLE_0:def_10 ::_thesis: Cl {(x . i)} c= pi ((Cl {x}),i) proof let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in pi ((Cl {x}),i) or a in Cl {(x . i)} ) assume a in pi ((Cl {x}),i) ; ::_thesis: a in Cl {(x . i)} then ex f being Function st ( f in Cl {x} & a = f . i ) by CARD_3:def_6; hence a in Cl {(x . i)} by Th29; ::_thesis: verum end; reconsider f = f as Element of (product J) by A1; let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in Cl {(x . i)} or a in pi ((Cl {x}),i) ) set y = f +* (i .--> a); A3: dom (Carrier J) = M by PARTFUN1:def_2; A4: f in product (Carrier J) by A2, WAYBEL18:def_3; then A5: dom f = M by A3, CARD_3:9; A6: dom (i .--> a) = {i} by FUNCOP_1:13; assume A7: a in Cl {(x . i)} ; ::_thesis: a in pi ((Cl {x}),i) A8: for m being set st m in dom (Carrier J) holds (f +* (i .--> a)) . m in (Carrier J) . m proof let m be set ; ::_thesis: ( m in dom (Carrier J) implies (f +* (i .--> a)) . m in (Carrier J) . m ) assume A9: m in dom (Carrier J) ; ::_thesis: (f +* (i .--> a)) . m in (Carrier J) . m then A10: ex R being 1-sorted st ( R = J . m & (Carrier J) . m = the carrier of R ) by PRALG_1:def_13; percases ( m = i or m <> i ) ; supposeA11: m = i ; ::_thesis: (f +* (i .--> a)) . m in (Carrier J) . m then (f +* (i .--> a)) . m = a by FUNCT_7:94; hence (f +* (i .--> a)) . m in (Carrier J) . m by A7, A10, A11; ::_thesis: verum end; suppose m <> i ; ::_thesis: (f +* (i .--> a)) . m in (Carrier J) . m then not m in dom (i .--> a) by A6, TARSKI:def_1; then (f +* (i .--> a)) . m = f . m by FUNCT_4:11; hence (f +* (i .--> a)) . m in (Carrier J) . m by A4, A9, CARD_3:9; ::_thesis: verum end; end; end; dom (f +* (i .--> a)) = (dom f) \/ (dom (i .--> a)) by FUNCT_4:def_1 .= M \/ {i} by A5, FUNCOP_1:13 .= M by ZFMISC_1:40 ; then f +* (i .--> a) in product (Carrier J) by A3, A8, CARD_3:9; then reconsider y = f +* (i .--> a) as Element of (product J) by WAYBEL18:def_3; for m being Element of M holds y . m in Cl {(x . m)} proof let m be Element of M; ::_thesis: y . m in Cl {(x . m)} percases ( m = i or m <> i ) ; suppose m = i ; ::_thesis: y . m in Cl {(x . m)} hence y . m in Cl {(x . m)} by A7, FUNCT_7:94; ::_thesis: verum end; suppose m <> i ; ::_thesis: y . m in Cl {(x . m)} then not m in dom (i .--> a) by A6, TARSKI:def_1; then y . m = f . m by FUNCT_4:11; hence y . m in Cl {(x . m)} by A1, Th29; ::_thesis: verum end; end; end; then A12: f +* (i .--> a) in Cl {x} by Th29; (f +* (i .--> a)) . i = a by FUNCT_7:94; hence a in pi ((Cl {x}),i) by A12, CARD_3:def_6; ::_thesis: verum end; theorem :: YELLOW14:32 for M being non empty set for i being Element of M for T being non empty TopSpace for x being Point of (product (M --> T)) holds pi ((Cl {x}),i) = Cl {(x . i)} proof let M be non empty set ; ::_thesis: for i being Element of M for T being non empty TopSpace for x being Point of (product (M --> T)) holds pi ((Cl {x}),i) = Cl {(x . i)} let i be Element of M; ::_thesis: for T being non empty TopSpace for x being Point of (product (M --> T)) holds pi ((Cl {x}),i) = Cl {(x . i)} let T be non empty TopSpace; ::_thesis: for x being Point of (product (M --> T)) holds pi ((Cl {x}),i) = Cl {(x . i)} let x be Point of (product (M --> T)); ::_thesis: pi ((Cl {x}),i) = Cl {(x . i)} (M --> T) . i = T by FUNCOP_1:7; hence pi ((Cl {x}),i) = Cl {(x . i)} by Th31; ::_thesis: verum end; theorem :: YELLOW14:33 for X, Y being non empty TopStruct for f being Function of X,Y for g being Function of Y,X st f = id X & g = id X & f is continuous & g is continuous holds TopStruct(# the carrier of X, the topology of X #) = TopStruct(# the carrier of Y, the topology of Y #) proof let X, Y be non empty TopStruct ; ::_thesis: for f being Function of X,Y for g being Function of Y,X st f = id X & g = id X & f is continuous & g is continuous holds TopStruct(# the carrier of X, the topology of X #) = TopStruct(# the carrier of Y, the topology of Y #) let f be Function of X,Y; ::_thesis: for g being Function of Y,X st f = id X & g = id X & f is continuous & g is continuous holds TopStruct(# the carrier of X, the topology of X #) = TopStruct(# the carrier of Y, the topology of Y #) let g be Function of Y,X; ::_thesis: ( f = id X & g = id X & f is continuous & g is continuous implies TopStruct(# the carrier of X, the topology of X #) = TopStruct(# the carrier of Y, the topology of Y #) ) assume that A1: f = id X and A2: g = id X and A3: f is continuous and A4: g is continuous ; ::_thesis: TopStruct(# the carrier of X, the topology of X #) = TopStruct(# the carrier of Y, the topology of Y #) A5: the carrier of X = dom f by FUNCT_2:def_1 .= the carrier of Y by A1, A2, FUNCT_2:def_1 ; A6: [#] Y <> {} ; A7: [#] X <> {} ; the topology of X = the topology of Y proof hereby :: according to TARSKI:def_3,XBOOLE_0:def_10 ::_thesis: the topology of Y c= the topology of X let A be set ; ::_thesis: ( A in the topology of X implies A in the topology of Y ) assume A8: A in the topology of X ; ::_thesis: A in the topology of Y then reconsider B = A as Subset of X ; B is open by A8, PRE_TOPC:def_2; then A9: g " B is open by A4, A7, TOPS_2:43; g " B = B by A2, FUNCT_2:94; hence A in the topology of Y by A9, PRE_TOPC:def_2; ::_thesis: verum end; let A be set ; :: according to TARSKI:def_3 ::_thesis: ( not A in the topology of Y or A in the topology of X ) assume A10: A in the topology of Y ; ::_thesis: A in the topology of X then reconsider B = A as Subset of Y ; B is open by A10, PRE_TOPC:def_2; then A11: f " B is open by A3, A6, TOPS_2:43; f " B = B by A1, A5, FUNCT_2:94; hence A in the topology of X by A11, PRE_TOPC:def_2; ::_thesis: verum end; hence TopStruct(# the carrier of X, the topology of X #) = TopStruct(# the carrier of Y, the topology of Y #) by A5; ::_thesis: verum end; theorem :: YELLOW14:34 for X, Y being non empty TopSpace for f being Function of X,Y st corestr f is continuous holds f is continuous proof let X, Y be non empty TopSpace; ::_thesis: for f being Function of X,Y st corestr f is continuous holds f is continuous let f be Function of X,Y; ::_thesis: ( corestr f is continuous implies f is continuous ) assume A1: corestr f is continuous ; ::_thesis: f is continuous corestr f = f by WAYBEL18:def_7; hence f is continuous by A1, PRE_TOPC:26; ::_thesis: verum end; registration let X be non empty TopSpace; let Y be non empty SubSpace of X; cluster incl Y -> continuous ; coherence incl Y is continuous by TMAP_1:87; end; theorem :: YELLOW14:35 for T being non empty TopSpace for f being Function of T,T st f * f = f holds (corestr f) * (incl (Image f)) = id (Image f) proof let T be non empty TopSpace; ::_thesis: for f being Function of T,T st f * f = f holds (corestr f) * (incl (Image f)) = id (Image f) let f be Function of T,T; ::_thesis: ( f * f = f implies (corestr f) * (incl (Image f)) = id (Image f) ) assume A1: f * f = f ; ::_thesis: (corestr f) * (incl (Image f)) = id (Image f) set cf = corestr f; set i = incl (Image f); for x being set st x in the carrier of (Image f) holds ((corestr f) * (incl (Image f))) . x = (id (Image f)) . x proof A2: the carrier of (Image f) c= the carrier of T by BORSUK_1:1; let x be set ; ::_thesis: ( x in the carrier of (Image f) implies ((corestr f) * (incl (Image f))) . x = (id (Image f)) . x ) assume A3: x in the carrier of (Image f) ; ::_thesis: ((corestr f) * (incl (Image f))) . x = (id (Image f)) . x the carrier of (Image f) = rng f by WAYBEL18:9; then A4: ex y being set st ( y in dom f & f . y = x ) by A3, FUNCT_1:def_3; thus ((corestr f) * (incl (Image f))) . x = (corestr f) . ((incl (Image f)) . x) by A3, FUNCT_2:15 .= (corestr f) . x by A3, A2, TMAP_1:84 .= f . x by WAYBEL18:def_7 .= x by A1, A4, FUNCT_2:15 .= (id (Image f)) . x by A3, FUNCT_1:18 ; ::_thesis: verum end; hence (corestr f) * (incl (Image f)) = id (Image f) by FUNCT_2:12; ::_thesis: verum end; theorem :: YELLOW14:36 for Y being non empty TopSpace for W being non empty SubSpace of Y holds corestr (incl W) is being_homeomorphism proof let Y be non empty TopSpace; ::_thesis: for W being non empty SubSpace of Y holds corestr (incl W) is being_homeomorphism let W be non empty SubSpace of Y; ::_thesis: corestr (incl W) is being_homeomorphism set ci = corestr (incl W); thus dom (corestr (incl W)) = [#] W by FUNCT_2:def_1; :: according to TOPS_2:def_5 ::_thesis: ( rng (corestr (incl W)) = [#] (Image (incl W)) & corestr (incl W) is one-to-one & corestr (incl W) is continuous & (corestr (incl W)) /" is continuous ) thus A1: rng (corestr (incl W)) = [#] (Image (incl W)) by FUNCT_2:def_3; ::_thesis: ( corestr (incl W) is one-to-one & corestr (incl W) is continuous & (corestr (incl W)) /" is continuous ) A2: corestr (incl W) = incl W by WAYBEL18:def_7 .= (id Y) | W by TMAP_1:def_6 .= (id the carrier of Y) | the carrier of W by TMAP_1:def_4 ; hence A3: corestr (incl W) is V14() by FUNCT_1:52; ::_thesis: ( corestr (incl W) is continuous & (corestr (incl W)) /" is continuous ) A4: for P being Subset of W st P is open holds ((corestr (incl W)) /") " P is open proof let P be Subset of W; ::_thesis: ( P is open implies ((corestr (incl W)) /") " P is open ) assume P in the topology of W ; :: according to PRE_TOPC:def_2 ::_thesis: ((corestr (incl W)) /") " P is open then A5: ex Q being Subset of Y st ( Q in the topology of Y & P = Q /\ ([#] W) ) by PRE_TOPC:def_4; A6: the carrier of W is non empty Subset of Y by BORSUK_1:1; then A7: P is Subset of Y by XBOOLE_1:1; A8: [#] W = rng ((id the carrier of Y) | the carrier of W) by A6, Th2 .= rng ((id Y) | W) by TMAP_1:def_4 .= rng (incl W) by TMAP_1:def_6 .= [#] (Image (incl W)) by WAYBEL18:9 ; ((corestr (incl W)) /") " P = ((id the carrier of Y) | the carrier of W) .: P by A1, A2, A3, TOPS_2:54 .= (id the carrier of Y) .: P by FUNCT_2:97 .= P by A7, FUNCT_1:92 ; hence ((corestr (incl W)) /") " P in the topology of (Image (incl W)) by A5, A8, PRE_TOPC:def_4; :: according to PRE_TOPC:def_2 ::_thesis: verum end; thus corestr (incl W) is continuous by WAYBEL18:10; ::_thesis: (corestr (incl W)) /" is continuous [#] W <> {} ; hence (corestr (incl W)) /" is continuous by A4, TOPS_2:43; ::_thesis: verum end; theorem Th37: :: YELLOW14:37 for M being non empty set for J being non-Empty TopStruct-yielding ManySortedSet of M st ( for i being Element of M holds J . i is T_0 TopSpace ) holds product J is T_0 proof let M be non empty set ; ::_thesis: for J being non-Empty TopStruct-yielding ManySortedSet of M st ( for i being Element of M holds J . i is T_0 TopSpace ) holds product J is T_0 let J be non-Empty TopStruct-yielding ManySortedSet of M; ::_thesis: ( ( for i being Element of M holds J . i is T_0 TopSpace ) implies product J is T_0 ) assume A1: for i being Element of M holds J . i is T_0 TopSpace ; ::_thesis: product J is T_0 for x, y being Point of (product J) st x <> y holds Cl {x} <> Cl {y} proof let x, y be Point of (product J); ::_thesis: ( x <> y implies Cl {x} <> Cl {y} ) assume that A2: x <> y and A3: Cl {x} = Cl {y} ; ::_thesis: contradiction y in the carrier of (product J) ; then y in product (Carrier J) by WAYBEL18:def_3; then dom y = dom (Carrier J) by CARD_3:9; then A4: dom y = M by PARTFUN1:def_2; x in the carrier of (product J) ; then x in product (Carrier J) by WAYBEL18:def_3; then dom x = dom (Carrier J) by CARD_3:9; then dom x = M by PARTFUN1:def_2; then consider i being set such that A5: i in M and A6: x . i <> y . i by A2, A4, FUNCT_1:2; reconsider i = i as Element of M by A5; A7: pi ((Cl {y}),i) = Cl {(y . i)} by Th31; ( J . i is T_0 TopSpace & pi ((Cl {x}),i) = Cl {(x . i)} ) by A1, Th31; hence contradiction by A3, A6, A7, TSP_1:def_5; ::_thesis: verum end; hence product J is T_0 by TSP_1:def_5; ::_thesis: verum end; registration let I be non empty set ; let T be non empty T_0 TopSpace; cluster product (I --> T) -> T_0 ; coherence product (I --> T) is T_0 proof for i being Element of I holds (I --> T) . i is T_0 TopSpace by FUNCOP_1:7; hence product (I --> T) is T_0 by Th37; ::_thesis: verum end; end; theorem Th38: :: YELLOW14:38 for M being non empty set for J being non-Empty TopStruct-yielding ManySortedSet of M st ( for i being Element of M holds ( J . i is T_1 & J . i is TopSpace-like ) ) holds product J is T_1 proof let M be non empty set ; ::_thesis: for J being non-Empty TopStruct-yielding ManySortedSet of M st ( for i being Element of M holds ( J . i is T_1 & J . i is TopSpace-like ) ) holds product J is T_1 let J be non-Empty TopStruct-yielding ManySortedSet of M; ::_thesis: ( ( for i being Element of M holds ( J . i is T_1 & J . i is TopSpace-like ) ) implies product J is T_1 ) assume A1: for i being Element of M holds ( J . i is T_1 & J . i is TopSpace-like ) ; ::_thesis: product J is T_1 for p being Point of (product J) holds {p} is closed proof let p be Point of (product J); ::_thesis: {p} is closed {p} = Cl {p} proof thus {p} c= Cl {p} by PRE_TOPC:18; :: according to XBOOLE_0:def_10 ::_thesis: Cl {p} c= {p} let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in Cl {p} or a in {p} ) assume A2: a in Cl {p} ; ::_thesis: a in {p} then reconsider a = a, p = p as Element of (product J) ; A3: for i being set st i in M holds a . i = p . i proof let i be set ; ::_thesis: ( i in M implies a . i = p . i ) assume i in M ; ::_thesis: a . i = p . i then reconsider i = i as Element of M ; ( J . i is TopSpace & J . i is T_1 ) by A1; then A4: {(p . i)} is closed by URYSOHN1:19; a . i in Cl {(p . i)} by A2, Th29; then a . i in {(p . i)} by A4, PRE_TOPC:22; hence a . i = p . i by TARSKI:def_1; ::_thesis: verum end; p in the carrier of (product J) ; then p in product (Carrier J) by WAYBEL18:def_3; then dom p = dom (Carrier J) by CARD_3:9; then A5: dom p = M by PARTFUN1:def_2; a in the carrier of (product J) ; then a in product (Carrier J) by WAYBEL18:def_3; then dom a = dom (Carrier J) by CARD_3:9; then dom a = M by PARTFUN1:def_2; then a = p by A5, A3, FUNCT_1:2; hence a in {p} by TARSKI:def_1; ::_thesis: verum end; hence {p} is closed ; ::_thesis: verum end; hence product J is T_1 by URYSOHN1:19; ::_thesis: verum end; registration let I be non empty set ; let T be non empty T_1 TopSpace; cluster product (I --> T) -> T_1 ; coherence product (I --> T) is T_1 proof for i being Element of I holds ( (I --> T) . i is T_1 & (I --> T) . i is TopSpace-like ) by FUNCOP_1:7; hence product (I --> T) is T_1 by Th38; ::_thesis: verum end; end;