let T be T_0-TopSpace; :: thesis: ( S1[T] iff S2[T] )
thus ( S1[T] implies S2[T] ) :: thesis: ( S2[T] implies S1[T] )
proof
assume A1: S1[T] ; :: thesis: S2[T]
let X be non empty TopSpace; :: thesis: 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; :: thesis: 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); :: thesis: 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 ;
then S is non empty full SubRelStr of L |^ the carrier of T by ;
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 ;
then A9: ( f is monotone & g is monotone ) by ;
take f ; :: thesis: 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 ; :: thesis: ( 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
.= 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 ;
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 ;
then g = f " by ;
hence ( f is uncurrying & f is isomorphic ) by ; :: thesis: ( g is currying & g is isomorphic )
A12: rng g = the carrier of (ContMaps (X,S)) by
.= 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 ;
then f = g " by ;
hence ( g is currying & g is isomorphic ) by ; :: thesis: verum
end;
assume A13: S2[T] ; :: thesis: S1[T]
let X be non empty TopSpace; :: thesis: 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; :: thesis: 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); :: thesis: 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 ; :: thesis: 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 ; :: thesis: ( 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; :: thesis: ( g is currying & g is V7() & g is onto )
thus ( g is currying & g is V7() & g is onto ) by A15; :: thesis: verum