let S be Subset of R^1; :: thesis: ( S = RAT implies for T being connected TopSpace
for f being Function of T,(R^1 | S) st f is continuous holds
f is constant )
assume A1: S = RAT ; :: thesis: for T being connected TopSpace
for f being Function of T,(R^1 | S) st f is continuous holds
f is constant
let T be connected TopSpace; :: thesis: for f being Function of T,(R^1 | S) st f is continuous holds
f is constant
let f be Function of T,(R^1 | S); :: thesis: ( f is continuous implies f is constant )
assume A2: f is continuous ; :: thesis: f is constant
per cases ( not T is empty or T is empty ) ;
suppose A3: not T is empty ; :: thesis: f is constant
set GX = Image f;
let x, y be object ; :: according to FUNCT_1:def 10 :: thesis: ( not x in dom f or not y in dom f or f . x = f . y )
assume that
A4: ( x in dom f & y in dom f ) and
A5: f . x <> f . y ; :: thesis: contradiction
per cases ( f . x < f . y or f . y < f . x ) by A5, XXREAL_0:1;
suppose f . x < f . y ; :: thesis: contradiction
then ex Q1, Q2 being Subset of (Image f) st
( Q1 misses Q2 & Q1 <> {} (Image f) & Q2 <> {} (Image f) & Q1 is open & Q2 is open & [#] (Image f) = Q1 \/ Q2 ) by A1, A3, A4, Lm9;
hence contradiction by A1, A2, A3, CONNSP_1:11; :: thesis: verum
end;
suppose f . y < f . x ; :: thesis: contradiction
then ex Q1, Q2 being Subset of (Image f) st
( Q1 misses Q2 & Q1 <> {} (Image f) & Q2 <> {} (Image f) & Q1 is open & Q2 is open & [#] (Image f) = Q1 \/ Q2 ) by A1, A3, A4, Lm9;
hence contradiction by A1, A2, A3, CONNSP_1:11; :: thesis: verum
end;
end;
end;
suppose T is empty ; :: thesis: f is constant
hence f is constant ; :: thesis: verum
end;
end;