let f be PartFunc of REAL,REAL; :: thesis: for N being open Subset of REAL st dom f = REAL & f is continuous holds
f " N is open
let N be open Subset of REAL; :: thesis: ( dom f = REAL & f is continuous implies f " N is open )
assume A1: ( dom f = REAL & f is continuous ) ; :: thesis: f " N is open
reconsider M = f " N as Subset of REAL ;

now :: thesis: for r being Element of REAL st r in M holds
ex K being Neighbourhood of r st K c= M

let r be Element of REAL ; :: thesis: ( r in M implies ex K being Neighbourhood of r st K c= M )
assume r in M ; :: thesis: ex K being Neighbourhood of r st K c= M
then ( r in dom f & f . r in N ) by FUNCT_1:def 7;
then consider g being Real such that
A5: ( 0 < g & ].((f . r) - g),((f . r) + g).[ c= N ) by RCOMP_1:19;
set N1 = ].((f . r) - g),((f . r) + g).[;
].((f . r) - g),((f . r) + g).[ is Neighbourhood of f . r by A5, RCOMP_1:def 6;
then consider K being Neighbourhood of r such that
A6: f .: K c= ].((f . r) - g),((f . r) + g).[ by A1, FCONT_1:5;
take K = K; :: thesis: K c= M
thus K c= M :: thesis: verum

proof

let s be object ; :: according to TARSKI:def 3 :: thesis: ( not s in K or s in M )
assume A7: s in K ; :: thesis: s in M
then f . s in f .: K by A1, FUNCT_1:def 6;
then f . s in ].((f . r) - g),((f . r) + g).[ by A6;
hence s in M by A1, A5, A7, FUNCT_1:def 7; :: thesis: verum

end;

end;

hence f " N is open by RCOMP_1:20; :: thesis: verum