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 <= 1 & P1 = { q0 where q0 is Point of (TOP-REAL 2) : ex ss being Real st
( 0 <= ss & ss < s & q0 = f . ss ) } & Q = [.0,s.[ 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 <= 1 & P1 = { q0 where q0 is Point of (TOP-REAL 2) : ex ss being Real st
( 0 <= ss & ss < s & q0 = f . ss ) } & Q = [.0,s.[ 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 <= 1 & P1 = { q0 where q0 is Point of (TOP-REAL 2) : ex ss being Real st
( 0 <= ss & ss < s & q0 = f . ss ) } & Q = [.0,s.[ holds
f .: Q = P1
let f be Function of I[01],((TOP-REAL 2) | P); :: thesis: for s being Real st s <= 1 & P1 = { q0 where q0 is Point of (TOP-REAL 2) : ex ss being Real st
( 0 <= ss & ss < s & q0 = f . ss ) } & Q = [.0,s.[ holds
f .: Q = P1
let s be Real; :: thesis: ( s <= 1 & P1 = { q0 where q0 is Point of (TOP-REAL 2) : ex ss being Real st
( 0 <= ss & ss < s & q0 = f . ss ) } & Q = [.0,s.[ implies f .: Q = P1 )
assume that
A1: s <= 1 and
A2: P1 = { q0 where q0 is Point of (TOP-REAL 2) : ex ss being Real st
( 0 <= ss & ss < s & q0 = f . ss ) } and
A3: Q = [.0,s.[ ; :: 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) ;
( 0 <= ss & ss < s ) by A3, A7, XXREAL_1:3;
then ex ss being Real st
( 0 <= ss & ss < s & 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 )
A9: dom f = [.0,1.] by BORSUK_1:40, FUNCT_2:def 1;
assume x in P1 ; :: thesis: x in f .: Q
then consider q0 being Point of (TOP-REAL 2) such that
A10: q0 = x and
A11: ex ss being Real st
( 0 <= ss & ss < s & q0 = f . ss ) by A2;
consider ss being Real such that
A12: 0 <= ss and
A13: ss < s and
A14: q0 = f . ss by A11;
ss < 1 by A1, A13, XXREAL_0:2;
then A15: ss in dom f by A12, A9, XXREAL_1:1;
ss in Q by A3, A12, A13, XXREAL_1:3;
hence x in f .: Q by A10, A14, A15, FUNCT_1:def 6; :: thesis: verum

end;

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