let P be non empty Subset of (TOP-REAL 2); :: thesis: for P1 being Subset of ((TOP-REAL 2) | P)
for Q being Subset of I[01]
for f being Function of I[01] ,((TOP-REAL 2) | P)
for s being Real st s >= 0 & P1 = { q0 where q0 is Point of (TOP-REAL 2) : ex ss being Real st
( s < ss & ss <= 1 & q0 = f . ss ) } & Q = ].s,1.] holds
f .: Q = P1
let P1 be Subset of ((TOP-REAL 2) | P); :: thesis: for Q being Subset of I[01]
for f being Function of I[01] ,((TOP-REAL 2) | P)
for s being Real st s >= 0 & P1 = { q0 where q0 is Point of (TOP-REAL 2) : ex ss being Real st
( s < ss & ss <= 1 & q0 = f . ss ) } & Q = ].s,1.] holds
f .: Q = P1
let Q be Subset of I[01] ; :: thesis: for f being Function of I[01] ,((TOP-REAL 2) | P)
for s being Real st s >= 0 & P1 = { q0 where q0 is Point of (TOP-REAL 2) : ex ss being Real st
( s < ss & ss <= 1 & q0 = f . ss ) } & Q = ].s,1.] holds
f .: Q = P1
let f be Function of I[01] ,((TOP-REAL 2) | P); :: thesis: for s being Real st s >= 0 & P1 = { q0 where q0 is Point of (TOP-REAL 2) : ex ss being Real st
( s < ss & ss <= 1 & q0 = f . ss ) } & Q = ].s,1.] holds
f .: Q = P1
let s be Real; :: thesis: ( s >= 0 & P1 = { q0 where q0 is Point of (TOP-REAL 2) : ex ss being Real st
( s < ss & ss <= 1 & q0 = f . ss ) } & Q = ].s,1.] implies f .: Q = P1 )
assume A1: ( s >= 0 & P1 = { q0 where q0 is Point of (TOP-REAL 2) : ex ss being Real st
( s < ss & ss <= 1 & q0 = f . ss ) } & Q = ].s,1.] ) ; :: thesis: f .: Q = P1
A2: the carrier of ((TOP-REAL 2) | P) = P by PRE_TOPC:29;
A3: P1 c= f .: Q

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in P1 or x in f .: Q )
assume x in P1 ; :: thesis: x in f .: Q
then consider q0 being Point of (TOP-REAL 2) such that
A4: ( q0 = x & ex ss being Real st
( s < ss & ss <= 1 & q0 = f . ss ) ) by A1;
consider ss being Real such that
A5: ( s < ss & ss <= 1 & q0 = f . ss ) by A4;
A6: ss in Q by A1, A5, XXREAL_1:2;
dom f = [.0 ,1.] by BORSUK_1:83, FUNCT_2:def 1;
then ss in dom f by A1, A5, XXREAL_1:1;
hence x in f .: Q by A4, A5, A6, FUNCT_1:def 12; :: thesis: verum

end;

f .: Q c= P1

proof

let y be set ; :: according to TARSKI:def 3 :: thesis: ( not y in f .: Q or y in P1 )
assume y in f .: Q ; :: thesis: y in P1
then consider z being set such that
A7: ( z in dom f & z in Q & f . z = y ) by FUNCT_1:def 12;
dom f = [.0 ,1.] by BORSUK_1:83, FUNCT_2:def 1;
then reconsider ss = z as Real by A7;
A8: ( s < ss & ss <= 1 ) by A1, A7, XXREAL_1:2;
y in rng f by A7, FUNCT_1:def 5;
then y in P by A2;
then reconsider q = y as Point of (TOP-REAL 2) ;
ex ss being Real st
( s < ss & ss <= 1 & q = f . ss ) by A7, A8;
hence y in P1 by A1; :: thesis: verum

end;

hence f .: Q = P1 by A3, XBOOLE_0:def 10; :: thesis: verum