let X be non empty TopSpace; :: thesis: for y being Complex
for f being Function of the carrier of X,COMPLEX st f = X --> y holds
f is continuous
let y be Complex; :: thesis: for f being Function of the carrier of X,COMPLEX st f = X --> y holds
f is continuous
let f be Function of the carrier of X,COMPLEX; :: thesis: ( f = X --> y implies f is continuous )
assume A1: f = X --> y ; :: thesis: f is continuous
set H = the carrier of X;
set HX = [#] X;
let P1 be Subset of COMPLEX; :: according to CC0SP2:def 1 :: thesis: ( P1 is closed implies f " P1 is closed )
assume P1 is closed ; :: thesis: f " P1 is closed

per cases ( y in P1 or not y in P1 ) ;

suppose y in P1 ; :: thesis: f " P1 is closed

then f " P1 = [#] X by A1, FUNCOP_1:14;
hence f " P1 is closed ; :: thesis: verum

end;

suppose not y in P1 ; :: thesis: f " P1 is closed

then f " P1 = {} X by A1, FUNCOP_1:16;
hence f " P1 is closed ; :: thesis: verum

end;

end;