set f = X --> y;
set HX = [#] X;
let P1 be Subset of REAL; :: according to PSCOMP_1:def 3 :: 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:14;
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:16;
hence (X --> y) " P1 is closed ; :: thesis: verum

end;

end;