let S, T be complete Scott TopLattice; :: thesis: SCMaps (S,T) = ContMaps (S,T)
reconsider Sm = ContMaps (S,T) as non empty full SubRelStr of T |^ the carrier of S by Def3;
reconsider SC = SCMaps (S,T) as non empty full SubRelStr of T |^ the carrier of S by WAYBEL15:1;
A1: the carrier of SC c= the carrier of (MonMaps (S,T)) by YELLOW_0:def 13;
A2: the carrier of SC c= the carrier of Sm
proof
let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in the carrier of SC or a in the carrier of Sm )
assume A3: a in the carrier of SC ; :: thesis: a in the carrier of Sm
then reconsider f = a as Function of S,T by A1, WAYBEL10:9;
f is continuous Function of S,T by A3, WAYBEL17:def 2;
then a is Element of Sm by Th21;
hence a in the carrier of Sm ; :: thesis: verum
end;
the carrier of Sm c= the carrier of SC
proof
let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in the carrier of Sm or a in the carrier of SC )
assume a in the carrier of Sm ; :: thesis: a in the carrier of SC
then a is continuous Function of S,T by Th21;
hence a in the carrier of SC by WAYBEL17:def 2; :: thesis: verum
end;
then the carrier of SC = the carrier of Sm by A2;
hence SCMaps (S,T) = ContMaps (S,T) by YELLOW_0:57; :: thesis: verum