let FT1, FT2 be non empty RelStr ; :: thesis: for A being Subset of FT1
for B being Subset of FT2
for f being Function of FT1,FT2 st f is_continuous 0 & B = f .: A holds
f .: (A ^b) c= B ^b
let A be Subset of FT1; :: thesis: for B being Subset of FT2
for f being Function of FT1,FT2 st f is_continuous 0 & B = f .: A holds
f .: (A ^b) c= B ^b
let B be Subset of FT2; :: thesis: for f being Function of FT1,FT2 st f is_continuous 0 & B = f .: A holds
f .: (A ^b) c= B ^b
let f be Function of FT1,FT2; :: thesis: ( f is_continuous 0 & B = f .: A implies f .: (A ^b) c= B ^b )
assume that
A1: f is_continuous 0 and
A2: B = f .: A ; :: thesis: f .: (A ^b) c= B ^b
thus f .: (A ^b) c= B ^b :: thesis: verum
proof
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in f .: (A ^b) or y in B ^b )
assume y in f .: (A ^b) ; :: thesis: y in B ^b
then consider x being object such that
A3: x in dom f and
A4: x in A ^b and
A5: y = f . x by FUNCT_1:def 6;
reconsider x0 = x as Element of FT1 by A3;
reconsider y0 = y as Element of FT2 by A3, A5, FUNCT_2:5;
f .: (U_FT (x0,0)) c= U_FT (y0,0) by A1, A5;
then f .: (U_FT x0) c= U_FT (y0,0) by FINTOPO3:47;
then f .: (U_FT x0) c= U_FT y0 by FINTOPO3:47;
then A6: ( f .: ((U_FT x0) /\ A) c= (f .: (U_FT x0)) /\ (f .: A) & (f .: (U_FT x0)) /\ (f .: A) c= (U_FT y0) /\ (f .: A) ) by RELAT_1:121, XBOOLE_1:26;
ex z being Element of FT1 st
( z = x & U_FT z meets A ) by A4;
then A7: (U_FT x0) /\ A <> {} by XBOOLE_0:def 7;
dom f = the carrier of FT1 by FUNCT_2:def 1;
then f .: ((U_FT x0) /\ A) <> {} by A7, RELAT_1:119;
then (U_FT y0) /\ (f .: A) <> {} by A6;
then U_FT y0 meets B by A2, XBOOLE_0:def 7;
hence y in B ^b ; :: thesis: verum
end;