theorem :: WAYBEL29:24

for Y being T_0-TopSpace holds

( ( for X being non empty TopSpace

for L being Scott continuous complete TopLattice

for T being Scott TopAugmentation of ContMaps (Y,L) ex f being Function of (ContMaps (X,T)),(ContMaps ([:X,Y:],L)) ex g being Function of (ContMaps ([:X,Y:],L)),(ContMaps (X,T)) st

( f is uncurrying & f is V7() & f is onto & g is currying & g is V7() & g is onto ) ) iff for X being non empty TopSpace

for L being Scott continuous complete TopLattice

for T being Scott TopAugmentation of ContMaps (Y,L) ex f being Function of (ContMaps (X,T)),(ContMaps ([:X,Y:],L)) ex g being Function of (ContMaps ([:X,Y:],L)),(ContMaps (X,T)) st

( f is uncurrying & f is isomorphic & g is currying & g is isomorphic ) ) by Lm1;

( ( for X being non empty TopSpace

for L being Scott continuous complete TopLattice

for T being Scott TopAugmentation of ContMaps (Y,L) ex f being Function of (ContMaps (X,T)),(ContMaps ([:X,Y:],L)) ex g being Function of (ContMaps ([:X,Y:],L)),(ContMaps (X,T)) st

( f is uncurrying & f is V7() & f is onto & g is currying & g is V7() & g is onto ) ) iff for X being non empty TopSpace

for L being Scott continuous complete TopLattice

for T being Scott TopAugmentation of ContMaps (Y,L) ex f being Function of (ContMaps (X,T)),(ContMaps ([:X,Y:],L)) ex g being Function of (ContMaps ([:X,Y:],L)),(ContMaps (X,T)) st

( f is uncurrying & f is isomorphic & g is currying & g is isomorphic ) ) by Lm1;