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
one-to-one &
f is
onto )
and A3:
(
g is
currying &
g is
one-to-one &
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:41;
L |^ the
carrier of
[:X,T:] = L |^ [:the carrier of X,the carrier of T:]
by BORSUK_1:def 5;
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:41;
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)
by FUNCT_2:def 1;
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, XBOOLE_1:1;
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:63;
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:])
by FUNCT_2:def 1;
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 5;
then
f * g = id (dom g)
by A2, A3, A12, WAYBEL27:5;
then
f = g "
by A3, A12, FUNCT_1:63;
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 one-to-one & f is onto & g is currying & g is one-to-one & 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 one-to-one & f is onto & g is currying & g is one-to-one & 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 one-to-one & f is onto & g is currying & g is one-to-one & 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 one-to-one & f is onto & g is currying & g is one-to-one & g is onto )
take
g
; ( f is uncurrying & f is one-to-one & f is onto & g is currying & g is one-to-one & g is onto )
thus
( f is uncurrying & f is one-to-one & f is onto )
by A14; ( g is currying & g is one-to-one & g is onto )
thus
( g is currying & g is one-to-one & g is onto )
by A15; verum