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 #) & TopStruct(# the carrier of X, the topology of X #) = TopStruct(# the carrier of X, the topology of X #) ) by WAYBEL25:def 2;

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, 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, YELLOW12:36;
hence a is Element of (oContMaps (X,Y)) by Th1; :: thesis: verum