let a be Element of (ContMaps (S,T)); :: according to MONOID_0:def 1 :: thesis: a is set
ex a9 being Function of S,T st
( a9 = a & a9 is continuous ) by Def3;
hence a is set ; :: thesis: verum