let S, T be complete Scott TopLattice; UPS (S,T) = SCMaps (S,T)
A1:
the carrier of (UPS (S,T)) = the carrier of (SCMaps (S,T))
proof
thus
the
carrier of
(UPS (S,T)) c= the
carrier of
(SCMaps (S,T))
XBOOLE_0:def 10 the carrier of (SCMaps (S,T)) c= the carrier of (UPS (S,T))
let x be
object ;
TARSKI:def 3 ( not x in the carrier of (SCMaps (S,T)) or x in the carrier of (UPS (S,T)) )
assume A2:
x in the
carrier of
(SCMaps (S,T))
;
x in the carrier of (UPS (S,T))
the
carrier of
(SCMaps (S,T)) c= the
carrier of
(MonMaps (S,T))
by YELLOW_0:def 13;
then reconsider f =
x as
Function of
S,
T by A2, WAYBEL10:9;
f is
continuous
by A2, WAYBEL17:def 2;
hence
x in the
carrier of
(UPS (S,T))
by Def4;
verum
end;
then A3:
the carrier of (UPS (S,T)) c= the carrier of (MonMaps (S,T))
by YELLOW_0:def 13;
UPS (S,T) is full SubRelStr of T |^ the carrier of S
by Def4;
then the InternalRel of (UPS (S,T)) =
the InternalRel of (T |^ the carrier of S) |_2 the carrier of (UPS (S,T))
by YELLOW_0:def 14
.=
( the InternalRel of (T |^ the carrier of S) |_2 the carrier of (MonMaps (S,T))) |_2 the carrier of (UPS (S,T))
by A3, WELLORD1:22
.=
the InternalRel of (MonMaps (S,T)) |_2 the carrier of (SCMaps (S,T))
by A1, YELLOW_0:def 14
.=
the InternalRel of (SCMaps (S,T))
by YELLOW_0:def 14
;
hence
UPS (S,T) = SCMaps (S,T)
by A1; verum