let T be T_0-TopSpace; ( S1[T] iff S2[T] )
thus
( S1[T] implies S2[T] )
( S2[T] implies S1[T] )proof
assume A1:
S1[
T]
;
S2[T]
let X be non
empty TopSpace;
for L being Scott continuous complete TopLattice
for T being Scott TopAugmentation of ContMaps (T,L) ex f being Function of (ContMaps (X,T)),(ContMaps ([:X,T:],L)) ex g being Function of (ContMaps ([:X,T:],L)),(ContMaps (X,T)) st
( f is uncurrying & f is isomorphic & g is currying & g is isomorphic )let L be
Scott continuous complete TopLattice;
for T being Scott TopAugmentation of ContMaps (T,L) ex f being Function of (ContMaps (X,T)),(ContMaps ([:X,T:],L)) ex g being Function of (ContMaps ([:X,T:],L)),(ContMaps (X,T)) st
( f is uncurrying & f is isomorphic & g is currying & g is isomorphic )let S be
Scott TopAugmentation of
ContMaps (
T,
L);
ex f being Function of (ContMaps (X,S)),(ContMaps ([:X,T:],L)) ex g being Function of (ContMaps ([:X,T:],L)),(ContMaps (X,S)) st
( f is uncurrying & f is isomorphic & g is currying & g is isomorphic )
consider f being
Function of
(ContMaps (X,S)),
(ContMaps ([:X,T:],L)),
g being
Function of
(ContMaps ([:X,T:],L)),
(ContMaps (X,S)) such that A2:
(
f is
uncurrying &
f is
V7() &
f is
onto )
and A3:
(
g is
currying &
g is
V7() &
g is
onto )
by A1;
A4:
RelStr(# the
carrier of
S, the
InternalRel of
S #)
= RelStr(# the
carrier of
(ContMaps (T,L)), the
InternalRel of
(ContMaps (T,L)) #)
by YELLOW_9:def 4;
A5:
ContMaps (
T,
L) is non
empty full SubRelStr of
L |^ the
carrier of
T
by WAYBEL24:def 3;
then A6:
the
InternalRel of
(ContMaps (T,L)) = the
InternalRel of
(L |^ the carrier of T) |_2 the
carrier of
(ContMaps (T,L))
by YELLOW_0:def 14;
( the
carrier of
(ContMaps (T,L)) c= the
carrier of
(L |^ the carrier of T) & the
InternalRel of
(ContMaps (T,L)) c= the
InternalRel of
(L |^ the carrier of T) )
by A5, YELLOW_0:def 13;
then
S is non
empty full SubRelStr of
L |^ the
carrier of
T
by A4, A6, YELLOW_0:def 13, YELLOW_0:def 14;
then A7:
S |^ the
carrier of
X is non
empty full SubRelStr of
(L |^ the carrier of T) |^ the
carrier of
X
by YELLOW16:39;
L |^ the
carrier of
[:X,T:] = L |^ [: the carrier of X, the carrier of T:]
by BORSUK_1:def 2;
then A8:
ContMaps (
[:X,T:],
L) is non
empty full SubRelStr of
L |^ [: the carrier of X, the carrier of T:]
by WAYBEL24:def 3;
ContMaps (
X,
S) is non
empty full SubRelStr of
S |^ the
carrier of
X
by WAYBEL24:def 3;
then
ContMaps (
X,
S) is non
empty full SubRelStr of
(L |^ the carrier of T) |^ the
carrier of
X
by A7, WAYBEL15:1;
then A9:
(
f is
monotone &
g is
monotone )
by A2, A3, A8, WAYBEL27:20, WAYBEL27:21;
take
f
;
ex g being Function of (ContMaps ([:X,T:],L)),(ContMaps (X,S)) st
( f is uncurrying & f is isomorphic & g is currying & g is isomorphic )
take
g
;
( f is uncurrying & f is isomorphic & g is currying & g is isomorphic )
ContMaps (
T,
L) is non
empty full SubRelStr of
L |^ the
carrier of
T
by WAYBEL24:def 3;
then
(ContMaps (T,L)) |^ the
carrier of
X is
full SubRelStr of
(L |^ the carrier of T) |^ the
carrier of
X
by YELLOW16:39;
then A10:
the
carrier of
((ContMaps (T,L)) |^ the carrier of X) c= the
carrier of
((L |^ the carrier of T) |^ the carrier of X)
by YELLOW_0:def 13;
A11:
rng f =
the
carrier of
(ContMaps ([:X,T:],L))
by A2, FUNCT_2:def 3
.=
dom g
by FUNCT_2:def 1
;
ContMaps (
X,
S) is non
empty full SubRelStr of
S |^ the
carrier of
X
by WAYBEL24:def 3;
then
the
carrier of
(ContMaps (X,S)) c= the
carrier of
(S |^ the carrier of X)
by YELLOW_0:def 13;
then
dom f c= the
carrier of
(S |^ the carrier of X)
;
then
dom f c= the
carrier of
((ContMaps (T,L)) |^ the carrier of X)
by A4, WAYBEL27:15;
then
dom f c= the
carrier of
((L |^ the carrier of T) |^ the carrier of X)
by A10;
then
dom f c= Funcs ( the
carrier of
X, the
carrier of
(L |^ the carrier of T))
by YELLOW_1:28;
then
dom f c= Funcs ( the
carrier of
X,
(Funcs ( the carrier of T, the carrier of L)))
by YELLOW_1:28;
then
g * f = id (dom f)
by A2, A3, A11, WAYBEL27:4;
then
g = f "
by A2, A11, FUNCT_1:41;
hence
(
f is
uncurrying &
f is
isomorphic )
by A2, A9, WAYBEL_0:def 38;
( g is currying & g is isomorphic )
A12:
rng g =
the
carrier of
(ContMaps (X,S))
by A3, FUNCT_2:def 3
.=
dom f
by FUNCT_2:def 1
;
ContMaps (
[:X,T:],
L) is non
empty full SubRelStr of
L |^ the
carrier of
[:X,T:]
by WAYBEL24:def 3;
then
the
carrier of
(ContMaps ([:X,T:],L)) c= the
carrier of
(L |^ the carrier of [:X,T:])
by YELLOW_0:def 13;
then
dom g c= the
carrier of
(L |^ the carrier of [:X,T:])
;
then
dom g c= Funcs ( the
carrier of
[:X,T:], the
carrier of
L)
by YELLOW_1:28;
then
dom g c= Funcs (
[: the carrier of X, the carrier of T:], the
carrier of
L)
by BORSUK_1:def 2;
then
f * g = id (dom g)
by A2, A3, A12, WAYBEL27:5;
then
f = g "
by A3, A12, FUNCT_1:41;
hence
(
g is
currying &
g is
isomorphic )
by A3, A9, WAYBEL_0:def 38;
verum
end;
assume A13:
S2[T]
; S1[T]
let X be non empty TopSpace; for L being Scott continuous complete TopLattice
for T being Scott TopAugmentation of ContMaps (T,L) ex f being Function of (ContMaps (X,T)),(ContMaps ([:X,T:],L)) ex g being Function of (ContMaps ([:X,T:],L)),(ContMaps (X,T)) st
( f is uncurrying & f is V7() & f is onto & g is currying & g is V7() & g is onto )
let L be Scott continuous complete TopLattice; for T being Scott TopAugmentation of ContMaps (T,L) ex f being Function of (ContMaps (X,T)),(ContMaps ([:X,T:],L)) ex g being Function of (ContMaps ([:X,T:],L)),(ContMaps (X,T)) st
( f is uncurrying & f is V7() & f is onto & g is currying & g is V7() & g is onto )
let S be Scott TopAugmentation of ContMaps (T,L); ex f being Function of (ContMaps (X,S)),(ContMaps ([:X,T:],L)) ex g being Function of (ContMaps ([:X,T:],L)),(ContMaps (X,S)) st
( f is uncurrying & f is V7() & f is onto & g is currying & g is V7() & g is onto )
consider f being Function of (ContMaps (X,S)),(ContMaps ([:X,T:],L)), g being Function of (ContMaps ([:X,T:],L)),(ContMaps (X,S)) such that
A14:
( f is uncurrying & f is isomorphic )
and
A15:
( g is currying & g is isomorphic )
by A13;
take
f
; ex g being Function of (ContMaps ([:X,T:],L)),(ContMaps (X,S)) st
( f is uncurrying & f is V7() & f is onto & g is currying & g is V7() & g is onto )
take
g
; ( f is uncurrying & f is V7() & f is onto & g is currying & g is V7() & g is onto )
thus
( f is uncurrying & f is V7() & f is onto )
by A14; ( g is currying & g is V7() & g is onto )
thus
( g is currying & g is V7() & g is onto )
by A15; verum