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,Y )
let a be set ; :: thesis: ( a is Element of (oContMaps X,Y) iff a is continuous Function of X,Y )
A1: TopStruct(# the carrier of (Omega Y),the topology of (Omega Y) #) = TopStruct(# the carrier of Y,the topology of Y #) by WAYBEL25:def 2;
A2: TopStruct(# the carrier of X,the topology of X #) = TopStruct(# the carrier of X,the topology of X #) ;

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

assume a is Element of (oContMaps X,Y) ; :: thesis: a is continuous Function of X,Y
then a is continuous Function of X,(Omega Y) by Th1;
hence a is continuous Function of X,Y by A1, A2, YELLOW12:36; :: thesis: verum

end;

assume a is continuous Function of X,Y ; :: thesis: a is Element of (oContMaps X,Y)
then a is continuous Function of X,(Omega Y) by A1, A2, YELLOW12:36;
hence a is Element of (oContMaps X,Y) by Th1; :: thesis: verum