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