let P be non empty Subset of (TOP-REAL 2); 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); 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]; 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); 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; ( 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.[
; f .: Q = P1
A4:
the carrier of ((TOP-REAL 2) | P) = P
by PRE_TOPC:8;
A5:
f .: Q c= P1
P1 c= f .: Q
proof
let x be
object ;
TARSKI:def 3 ( 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
;
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;
verum
end;
hence
f .: Q = P1
by A5, XBOOLE_0:def 10; verum