let P be non empty Subset of (TOP-REAL 2); :: thesis:
let P1 be Subset of ((TOP-REAL 2) | P); :: thesis:
let Q be Subset of I[01]; :: thesis:
let f be Function of I[01],((TOP-REAL 2) | P); :: thesis:
let s be Real; :: thesis:
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:
A4: the carrier of ((TOP-REAL 2) | P) = P by PRE_TOPC:8;
A5: f .: Q c= P1

let y be object ; :: according to TARSKI:def 3 :: thesis:
assume y in f .: Q ; :: thesis:
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:

end;

P1 c= f .: Q

let x be object ; :: according to TARSKI:def 3 :: thesis:
assume x in P1 ; :: thesis:
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:

end;