let T be non empty TopSpace; :: thesis:
assume A1: T is compact ; :: thesis:
let f be RealMap of T; :: according to PSCOMP_1:def 4 :: thesis:
assume A2: f is continuous ; :: thesis:
thus f is V49() :: according to SEQ_2:def 8 :: thesis:

proof

set p = the Element of T;
defpred S₁[ Real] means c₁ >= f . the Element of T;
set R = { (right_closed_halfline r3) where r3 is Element of REAL : S₁[r3] } ;
A3: { (right_closed_halfline r3) where r3 is Element of REAL : S₁[r3] } is Subset-Family of REAL from DOMAIN_1:sch 8();
A4: right_closed_halfline (f . the Element of T) in { (right_closed_halfline r3) where r3 is Element of REAL : S₁[r3] } ;
then reconsider R = { (right_closed_halfline r3) where r3 is Element of REAL : S₁[r3] } as non empty Subset-Family of REAL by A3;
reconsider F = (" f) .: R as Subset-Family of T ;
A5: F is c=-linear

proof

let X, Y be set ; :: according to ORDINAL1:def 8 :: thesis:
assume X in F ; :: thesis:
then consider A being object such that
A6: A in bool REAL and
A7: A in R and
A8: X = (" f) . A by FUNCT_2:64;
reconsider A = A as set by TARSKI:1;
A9: X = f " A by A6, A8, MEASURE6:def 3;
consider r1 being Element of REAL such that
A10: A = right_closed_halfline r1 and
r1 >= f . the Element of T by A7;
assume Y in F ; :: thesis:
then consider B being object such that
A11: B in bool REAL and
A12: B in R and
A13: Y = (" f) . B by FUNCT_2:64;
reconsider B = B as set by TARSKI:1;
A14: Y = f " B by A11, A13, MEASURE6:def 3;
consider r2 being Element of REAL such that
A15: B = right_closed_halfline r2 and
r2 >= f . the Element of T by A12;
( r1 >= r2 or r2 >= r1 ) ;
then ( X c= Y or Y c= X ) by A10, A15, A9, A14, RELAT_1:143, XXREAL_1:38;
hence X,Y are_c=-comparable by XBOOLE_0:def 9; :: thesis:

end;

assume A16: for s being Real holds s is not UpperBound of f .: the carrier of T ; :: according to XXREAL_2:def 10,MEASURE6:def 11 :: thesis:

now :: thesis:

assume {} in F ; :: thesis:
then consider rchx being object such that
A17: rchx in bool REAL and
A18: rchx in R and
A19: {} = (" f) . rchx by FUNCT_2:64;
consider r3 being Element of REAL such that
A20: rchx = right_closed_halfline r3 and
r3 >= f . the Element of T by A18;
r3 is not UpperBound of f .: the carrier of T by A16;
then consider r1 being ExtReal such that
A21: r1 in f .: the carrier of T and
A22: r1 > r3 by XXREAL_2:def 1;
reconsider rchx = rchx as set by TARSKI:1;
rchx = { g where g is Real : g >= r3 } by A20, XXREAL_1:232;
then A23: r1 in rchx by A21, A22;
A24: ex c being object st
( c in the carrier of T & c in the carrier of T & r1 = f . c ) by A21, FUNCT_2:64;
{} = f " rchx by A17, A19, MEASURE6:def 3;
hence contradiction by A24, A23, FUNCT_2:38; :: thesis:

end;

then A25: F is with_non-empty_elements by SETFAM_1:def 8;
R is closed

proof

let X be Subset of REAL; :: according to MEASURE6:def 7 :: thesis:
assume X in R ; :: thesis:
then ex r3 being Element of REAL st
( X = right_closed_halfline r3 & r3 >= f . the Element of T ) ;
hence X is closed ; :: thesis:

end;

then A26: F is closed by A2, Th13;
(" f) . (right_closed_halfline (f . the Element of T)) in F by A4, FUNCT_2:35;
then meet F <> {} by A1, A25, A5, A26, COMPTS_1:4;
then consider x being object such that
A27: x in meet F by XBOOLE_0:def 1;
set eR = the Element of R;
the Element of R in R ;
then consider er being Element of REAL such that
A28: the Element of R = right_closed_halfline er and
A29: er >= f . the Element of T ;
reconsider x = x as Element of T by A27;
A30: f . x in meet R by A27, MEASURE6:35;
then A31: f . x in the Element of R by SETFAM_1:def 1;
consider fx9 being Real such that
A32: fx9 > f . x by XREAL_1:1;
reconsider fx9 = fx9 as Element of REAL by XREAL_0:def 1;
right_closed_halfline er = { r3 where r3 is Real : r3 >= er } by XXREAL_1:232;
then ex r1 being Real st
( f . x = r1 & r1 >= er ) by A31, A28;
then f . x >= f . the Element of T by A29, XXREAL_0:2;
then fx9 >= f . the Element of T by A32, XXREAL_0:2;
then right_closed_halfline fx9 in R ;
then A33: f . x in right_closed_halfline fx9 by A30, SETFAM_1:def 1;
right_closed_halfline fx9 = { r3 where r3 is Real : r3 >= fx9 } by XXREAL_1:232;
then ex r3 being Real st
( f . x = r3 & r3 >= fx9 ) by A33;
hence contradiction by A32; :: thesis:

end;

set p = the Element of T;
defpred S₁[ Real] means c₁ <= f . the Element of T;
set R = { (left_closed_halfline r3) where r3 is Element of REAL : S₁[r3] } ;
A34: { (left_closed_halfline r3) where r3 is Element of REAL : S₁[r3] } is Subset-Family of REAL from DOMAIN_1:sch 8();
A35: left_closed_halfline (f . the Element of T) in { (left_closed_halfline r3) where r3 is Element of REAL : S₁[r3] } ;
then reconsider R = { (left_closed_halfline r3) where r3 is Element of REAL : S₁[r3] } as non empty Subset-Family of REAL by A34;
reconsider F = (" f) .: R as Subset-Family of T ;
R is closed

proof

let X be Subset of REAL; :: according to MEASURE6:def 7 :: thesis:
assume X in R ; :: thesis:
then ex r3 being Element of REAL st
( X = left_closed_halfline r3 & r3 <= f . the Element of T ) ;
hence X is closed ; :: thesis:

end;

then A36: F is closed by A2, Th13;
A37: F is c=-linear

proof

let X, Y be set ; :: according to ORDINAL1:def 8 :: thesis:
assume X in F ; :: thesis:
then consider A being object such that
A38: A in bool REAL and
A39: A in R and
A40: X = (" f) . A by FUNCT_2:64;
reconsider A = A as set by TARSKI:1;
A41: X = f " A by A38, A40, MEASURE6:def 3;
consider r1 being Element of REAL such that
A42: A = left_closed_halfline r1 and
r1 <= f . the Element of T by A39;
assume Y in F ; :: thesis:
then consider B being object such that
A43: B in bool REAL and
A44: B in R and
A45: Y = (" f) . B by FUNCT_2:64;
reconsider B = B as set by TARSKI:1;
A46: Y = f " B by A43, A45, MEASURE6:def 3;
consider r2 being Element of REAL such that
A47: B = left_closed_halfline r2 and
r2 <= f . the Element of T by A44;
( r1 <= r2 or r2 <= r1 ) ;
then ( X c= Y or Y c= X ) by A42, A47, A41, A46, RELAT_1:143, XXREAL_1:42;
hence X,Y are_c=-comparable by XBOOLE_0:def 9; :: thesis:

end;

assume A48: for s being Real holds s is not LowerBound of f .: the carrier of T ; :: according to XXREAL_2:def 9,MEASURE6:def 10 :: thesis:

now :: thesis:

assume {} in F ; :: thesis:
then consider rchx being object such that
A49: rchx in bool REAL and
A50: rchx in R and
A51: {} = (" f) . rchx by FUNCT_2:64;
consider r3 being Element of REAL such that
A52: rchx = left_closed_halfline r3 and
r3 <= f . the Element of T by A50;
r3 is not LowerBound of f .: the carrier of T by A48;
then consider r1 being ExtReal such that
A53: r1 in f .: the carrier of T and
A54: r1 < r3 by XXREAL_2:def 2;
reconsider rchx = rchx as set by TARSKI:1;
rchx = { g where g is Real : g <= r3 } by A52, XXREAL_1:231;
then A55: r1 in rchx by A53, A54;
A56: ex c being object st
( c in the carrier of T & c in the carrier of T & r1 = f . c ) by A53, FUNCT_2:64;
{} = f " rchx by A49, A51, MEASURE6:def 3;
hence contradiction by A56, A55, FUNCT_2:38; :: thesis:

end;

then A57: F is with_non-empty_elements by SETFAM_1:def 8;
(" f) . (left_closed_halfline (f . the Element of T)) in F by A35, FUNCT_2:35;
then meet F <> {} by A1, A57, A37, A36, COMPTS_1:4;
then consider x being object such that
A58: x in meet F by XBOOLE_0:def 1;
set eR = the Element of R;
the Element of R in R ;
then consider er being Element of REAL such that
A59: the Element of R = left_closed_halfline er and
A60: er <= f . the Element of T ;
reconsider x = x as Element of T by A58;
A61: f . x in meet R by A58, MEASURE6:35;
then A62: f . x in the Element of R by SETFAM_1:def 1;
consider fx9 being Real such that
A63: fx9 < f . x by XREAL_1:2;
reconsider fx9 = fx9 as Element of REAL by XREAL_0:def 1;
left_closed_halfline er = { r3 where r3 is Real : r3 <= er } by XXREAL_1:231;
then ex r1 being Real st
( f . x = r1 & r1 <= er ) by A62, A59;
then f . x <= f . the Element of T by A60, XXREAL_0:2;
then fx9 <= f . the Element of T by A63, XXREAL_0:2;
then left_closed_halfline fx9 in R ;
then A64: f . x in left_closed_halfline fx9 by A61, SETFAM_1:def 1;
left_closed_halfline fx9 = { r3 where r3 is Real : r3 <= fx9 } by XXREAL_1:231;
then ex r3 being Real st
( f . x = r3 & r3 <= fx9 ) by A64;
hence contradiction by A63; :: thesis: