let n be Element of NAT ; :: thesis: for a, b being Real
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 = p /. i ) holds
f " { s where s is Real : ( a < s & s < b ) } = { p where p is Element of (TOP-REAL n) : ( a < p /. i & p /. i < b ) }
let a, b be Real; :: 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 = p /. i ) holds
f " { s where s is Real : ( a < s & s < b ) } = { p where p is Element of (TOP-REAL n) : ( a < p /. i & 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 = p /. i ) holds
f " { s where s is Real : ( a < s & s < b ) } = { p where p is Element of (TOP-REAL n) : ( a < p /. i & p /. i < b ) }
let i be Element of NAT ; :: thesis: ( ( for p being Element of (TOP-REAL n) holds f . p = p /. i ) implies f " { s where s is Real : ( a < s & s < b ) } = { p where p is Element of (TOP-REAL n) : ( a < p /. i & p /. i < b ) } )
assume A1: for p being Element of (TOP-REAL n) holds f . p = p /. i ; :: thesis: f " { s where s is Real : ( a < s & s < b ) } = { p where p is Element of (TOP-REAL n) : ( a < p /. i & p /. i < b ) }
thus f " { s where s is Real : ( a < s & s < b ) } = { p where p is Element of (TOP-REAL n) : ( a < p /. i & p /. i < b ) } :: thesis: verum

proof

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

proof

let x be object ; :: 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 < p /. i & p /. i < b ) } )
assume A3: 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 < p /. i & p /. i < b ) }
then reconsider px = x as Element of (TOP-REAL n) ;
f . x in { s where s is Real : ( a < s & s < b ) } by A3, FUNCT_1:def 7;
then A4: ex s being Real st
( s = f . x & a < s & s < b ) ;
f . px = px /. i by A1;
hence x in { p where p is Element of (TOP-REAL n) : ( a < p /. i & p /. i < b ) } by A4; :: thesis: verum

end;

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

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { p where p is Element of (TOP-REAL n) : ( a < p /. i & 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 < p /. i & 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 and
A7: ( a < p /. i & p /. i < b ) ;
f . x = p /. i by A1, A6;
then f . x in { s where s is Real : ( a < s & s < b ) } by A7;
hence x in f " { s where s is Real : ( a < s & s < b ) } by A5, A6, FUNCT_1:def 7; :: thesis: verum

end;

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

end;