let a be Element of (ContMaps S,T); :: according to MONOID_0:def 1 :: thesis: a is set
consider a' being Function of S,T such that
A1: ( a' = a & a' is continuous ) by Def3;
thus a is set by A1; :: thesis: verum