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;

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

( 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 continuous Function of X,Y
; :: thesis: 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;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

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