let X be TopSpace; :: thesis: for Y being non empty TopSpace
for y being Point of Y holds X --> y is continuous
let Y be non empty TopSpace; :: thesis: for y being Point of Y holds X --> y is continuous
let y be Point of Y; :: thesis: X --> y is continuous
set F = X --> y;
set H = [#] X;
let P1 be Subset of Y; :: according to PRE_TOPC:def 12 :: thesis: ( not P1 is closed or (X --> y) " P1 is closed )
assume P1 is closed ; :: thesis: (X --> y) " P1 is closed

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

suppose y in P1 ; :: thesis: (X --> y) " P1 is closed

then (X --> y) " P1 = [#] X by FUNCOP_1:20;
hence (X --> y) " P1 is closed ; :: thesis: verum

end;

suppose not y in P1 ; :: thesis: (X --> y) " P1 is closed

then (X --> y) " P1 = {} X by FUNCOP_1:22;
hence (X --> y) " P1 is closed ; :: thesis: verum

end;

end;