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 that
A1: s >= 0 and
A2: P1 = { q0 where q0 is Point of (TOP-REAL 2) : ex ss being Real st
( s < ss & ss <= 1 & q0 = f . ss ) } and
A3: Q = ].s,1.] ; :: thesis: f .: Q = P1
A4: the carrier of ((TOP-REAL 2) | P) = P by PRE_TOPC:8;
A5: f .: Q c= P1

proof

let y be object ; :: 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 object such that
A6: z in dom f and
A7: z in Q and
A8: f . z = y by FUNCT_1:def 6;
reconsider ss = z as Real by A6;
y in rng f by A6, A8, FUNCT_1:def 3;
then y in P by A4;
then reconsider q = y as Point of (TOP-REAL 2) ;
( s < ss & ss <= 1 ) by A3, A7, XXREAL_1:2;
then ex ss being Real st
( s < ss & ss <= 1 & q = f . ss ) by A8;
hence y in P1 by A2; :: thesis: verum

end;

P1 c= f .: Q

proof

let x be object ; :: 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
A9: q0 = x and
A10: ex ss being Real st
( s < ss & ss <= 1 & q0 = f . ss ) by A2;
consider ss being Real such that
A11: ( s < ss & ss <= 1 ) and
A12: q0 = f . ss by A10;
A13: ss in Q by A3, A11, XXREAL_1:2;
dom f = [.0,1.] by BORSUK_1:40, FUNCT_2:def 1;
then ss in dom f by A1, A11, XXREAL_1:1;
hence x in f .: Q by A9, A12, A13, FUNCT_1:def 6; :: thesis: verum

end;

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