let X, Y be non empty TopSpace; :: thesis: for a being set holds
( a is Element of (oContMaps (X,Y)) iff a is continuous Function of X,(Omega Y) )
let a be set ; :: thesis: ( a is Element of (oContMaps (X,Y)) iff a is continuous Function of X,(Omega Y) )

hereby :: thesis: ( a is continuous Function of X,(Omega Y) implies a is Element of (oContMaps (X,Y)) )

assume a is Element of (oContMaps (X,Y)) ; :: thesis: a is continuous Function of X,(Omega Y)
then ex f being Function of X,(Omega Y) st
( a = f & f is continuous ) by WAYBEL24:def 3;
hence a is continuous Function of X,(Omega Y) ; :: thesis: verum

end;

assume a is continuous Function of X,(Omega Y) ; :: thesis: a is Element of (oContMaps (X,Y))
hence a is Element of (oContMaps (X,Y)) by WAYBEL24:def 3; :: thesis: verum