let X be non empty TopSpace; :: thesis: for S being Scott complete TopLattice holds oContMaps (X,S) = ContMaps (X,S)
let S be Scott complete TopLattice; :: thesis: 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 ; :: thesis: verum