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