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 A1: ( 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.[ ) ; :: 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
( 0 <= ss & ss < s & q0 = f . ss ) ) by A1;
consider ss being Real such that
A5: ( 0 <= ss & ss < s & q0 = f . ss ) by A4;
A6: ss < 1 by A1, A5, XXREAL_0:2;
A7: ss in Q by A1, A5, XXREAL_1:3;
dom f = [.0 ,1.] by BORSUK_1:83, FUNCT_2:def 1;
then ss in dom f by A5, A6, XXREAL_1:1;
hence x in f .: Q by A4, A5, A7, 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
A8: ( 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 A8;
A9: ( 0 <= ss & ss < s ) by A1, A8, XXREAL_1:3;
y in rng f by A8, 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
( 0 <= ss & ss < s & q = f . ss ) by A8, A9;
hence y in P1 by A1; :: thesis: verum

end;

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