let S be non empty TopSpace; for T being non empty TopSpace-like reflexive TopRelStr
for x being set holds
( x is continuous Function of S,T iff x is Element of (ContMaps (S,T)) )
let T be non empty TopSpace-like reflexive TopRelStr ; for x being set holds
( x is continuous Function of S,T iff x is Element of (ContMaps (S,T)) )
let x be set ; ( x is continuous Function of S,T iff x is Element of (ContMaps (S,T)) )
thus
( x is continuous Function of S,T implies x is Element of (ContMaps (S,T)) )
by Def3; ( x is Element of (ContMaps (S,T)) implies x is continuous Function of S,T )
assume
x is Element of (ContMaps (S,T))
; x is continuous Function of S,T
then
ex f being Function of S,T st
( x = f & f is continuous )
by Def3;
hence
x is continuous Function of S,T
; verum