let n be Element of NAT ; :: thesis: for a, b being real number
for f being Function of (TOP-REAL n),R^1
for i being Element of NAT st ( for p being Element of (TOP-REAL n) holds f . p = Proj p,i ) holds
f " { s where s is Real : ( a < s & s < b ) } = { p where p is Element of (TOP-REAL n) : ( a < Proj p,i & Proj p,i < b ) }
let a, b be real number ; :: thesis: for f being Function of (TOP-REAL n),R^1
for i being Element of NAT st ( for p being Element of (TOP-REAL n) holds f . p = Proj p,i ) holds
f " { s where s is Real : ( a < s & s < b ) } = { p where p is Element of (TOP-REAL n) : ( a < Proj p,i & Proj p,i < b ) }
let f be Function of (TOP-REAL n),R^1 ; :: thesis: for i being Element of NAT st ( for p being Element of (TOP-REAL n) holds f . p = Proj p,i ) holds
f " { s where s is Real : ( a < s & s < b ) } = { p where p is Element of (TOP-REAL n) : ( a < Proj p,i & Proj p,i < b ) }
let i be Element of NAT ; :: thesis: ( ( for p being Element of (TOP-REAL n) holds f . p = Proj p,i ) implies f " { s where s is Real : ( a < s & s < b ) } = { p where p is Element of (TOP-REAL n) : ( a < Proj p,i & Proj p,i < b ) } )
assume A1: for p being Element of (TOP-REAL n) holds f . p = Proj p,i ; :: thesis: f " { s where s is Real : ( a < s & s < b ) } = { p where p is Element of (TOP-REAL n) : ( a < Proj p,i & Proj p,i < b ) }
thus f " { s where s is Real : ( a < s & s < b ) } = { p where p is Element of (TOP-REAL n) : ( a < Proj p,i & Proj p,i < b ) } :: thesis: verum

proof

A2: dom f = the carrier of (TOP-REAL n) by FUNCT_2:def 1;
A3: f " { s where s is Real : ( a < s & s < b ) } c= { p where p is Element of (TOP-REAL n) : ( a < Proj p,i & Proj p,i < b ) }

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in f " { s where s is Real : ( a < s & s < b ) } or x in { p where p is Element of (TOP-REAL n) : ( a < Proj p,i & Proj p,i < b ) } )
assume A4: x in f " { s where s is Real : ( a < s & s < b ) } ; :: thesis: x in { p where p is Element of (TOP-REAL n) : ( a < Proj p,i & Proj p,i < b ) }
then ( x in dom f & f . x in { s where s is Real : ( a < s & s < b ) } ) by FUNCT_1:def 13;
then consider s being Real such that
A5: ( s = f . x & a < s & s < b ) ;
reconsider px = x as Element of (TOP-REAL n) by A4;
f . px = Proj px,i by A1;
hence x in { p where p is Element of (TOP-REAL n) : ( a < Proj p,i & Proj p,i < b ) } by A5; :: thesis: verum

end;

{ p where p is Element of (TOP-REAL n) : ( a < Proj p,i & Proj p,i < b ) } c= f " { s where s is Real : ( a < s & s < b ) }

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in { p where p is Element of (TOP-REAL n) : ( a < Proj p,i & Proj p,i < b ) } or x in f " { s where s is Real : ( a < s & s < b ) } )
assume x in { p where p is Element of (TOP-REAL n) : ( a < Proj p,i & Proj p,i < b ) } ; :: thesis: x in f " { s where s is Real : ( a < s & s < b ) }
then consider p being Element of (TOP-REAL n) such that
A6: ( x = p & a < Proj p,i & Proj p,i < b ) ;
f . x = Proj p,i by A1, A6;
then f . x in { s where s is Real : ( a < s & s < b ) } by A6;
hence x in f " { s where s is Real : ( a < s & s < b ) } by A2, A6, FUNCT_1:def 13; :: thesis: verum

end;

hence f " { s where s is Real : ( a < s & s < b ) } = { p where p is Element of (TOP-REAL n) : ( a < Proj p,i & Proj p,i < b ) } by A3, XBOOLE_0:def 10; :: thesis: verum

end;