let T be T_0-TopSpace; :: thesis: ( S_{1}[T] iff S_{2}[T] )

thus ( S_{1}[T] implies S_{2}[T] )
:: thesis: ( S_{2}[T] implies S_{1}[T] )_{2}[T]
; :: thesis: S_{1}[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

thus ( S

proof

assume A13:
S
assume A1:
S_{1}[T]
; :: thesis: S_{2}[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 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 ; :: 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 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; :: thesis: ( 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; :: thesis: verum

end;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 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 ; :: 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 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; :: thesis: ( 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; :: thesis: verum

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