let X be non empty TopSpace; for S being Scott complete TopLattice holds oContMaps (X,S) = ContMaps (X,S)
let S be Scott complete TopLattice; oContMaps (X,S) = ContMaps (X,S)
A1:
( Omega S = TopRelStr(# the carrier of S, the InternalRel of S, the topology of S #) & TopStruct(# the carrier of X, the topology of X #) = TopStruct(# the carrier of X, the topology of X #) )
by WAYBEL25:15;
thus oContMaps (X,S) =
ContMaps (X,(Omega S))
by WAYBEL26:def 1
.=
ContMaps (X,S)
by A1, Th10
; verum