let X, Y be non empty TopSpace; :: thesis: the carrier of (oContMaps (X,Y)) c= Funcs ( the carrier of X, the carrier of Y)

oContMaps (X,Y) is SubRelStr of (Omega Y) |^ the carrier of X by WAYBEL24:def 3;

then A1: the carrier of (oContMaps (X,Y)) c= the carrier of ((Omega Y) |^ the carrier of X) by YELLOW_0:def 13;

TopStruct(# the carrier of Y, the topology of Y #) = TopStruct(# the carrier of (Omega Y), the topology of (Omega Y) #) by WAYBEL25:def 2;

hence the carrier of (oContMaps (X,Y)) c= Funcs ( the carrier of X, the carrier of Y) by A1, YELLOW_1:28; :: thesis: verum

oContMaps (X,Y) is SubRelStr of (Omega Y) |^ the carrier of X by WAYBEL24:def 3;

then A1: the carrier of (oContMaps (X,Y)) c= the carrier of ((Omega Y) |^ the carrier of X) by YELLOW_0:def 13;

TopStruct(# the carrier of Y, the topology of Y #) = TopStruct(# the carrier of (Omega Y), the topology of (Omega Y) #) by WAYBEL25:def 2;

hence the carrier of (oContMaps (X,Y)) c= Funcs ( the carrier of X, the carrier of Y) by A1, YELLOW_1:28; :: thesis: verum