let S be non empty TopSpace; :: thesis: 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 ; :: thesis: for x being set holds
( x is continuous Function of S,T iff x is Element of (ContMaps S,T) )
let x be set ; :: thesis: ( 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; :: thesis: ( x is Element of (ContMaps S,T) implies x is continuous Function of S,T )
assume x is Element of (ContMaps S,T) ; :: thesis: x is continuous Function of S,T
then consider f being Function of S,T such that
A1: ( x = f & f is continuous ) by Def3;
thus x is continuous Function of S,T by A1; :: thesis: verum