let X be non empty TopSpace; :: thesis:
let R be non empty SubSpace of R^1 ; :: thesis:
let A be non empty finite set ; :: thesis:
let F be ManySortedFunction of A; :: thesis:
defpred S₁[ set ] means ( $1 is empty or ex f being continuous Function of X,R st
for x being Point of X
for S being non empty finite Subset of REAL st S = rng ((commute (F | $1)) . x) holds
f . x = max S );
A1: S₁[ {} ] ;
A2: dom F = A by PARTFUN1:def 2;
assume A3: for a being set st a in A holds
F . a is continuous Function of X,R ; :: thesis:
rng F c= Funcs ( the carrier of X, the carrier of R)

proof

let a be object ; :: according to TARSKI:def 3 :: thesis:
assume a in rng F ; :: thesis:
then ex b being object st
( b in dom F & a = F . b ) by FUNCT_1:def 3;
then a is Function of X,R by A3;
hence a in Funcs ( the carrier of X, the carrier of R) by FUNCT_2:8; :: thesis:

end;

then A4: F in Funcs (A,(Funcs ( the carrier of X, the carrier of R))) by A2, FUNCT_2:def 2;

A5: now :: thesis:

let x, B be set ; :: thesis:
assume A6: x in A ; :: thesis:
then reconsider fx = F . x as continuous Function of X,R by A3;
assume A7: B c= A ; :: thesis:
assume A8: S₁[B] ; :: thesis:

per cases ;

suppose A9: B = {} ; :: thesis:

thus S₁[B \/ {x}] :: thesis:

proof

assume not B \/ {x} is empty ; :: thesis:
take fx ; :: thesis:
let a be Point of X; :: thesis:
let S be non empty finite Subset of REAL; :: thesis:
A10: dom fx = the carrier of X by FUNCT_2:def 1;
F | {x} = x .--> (F . x) by A2, A6, FUNCT_7:6;
then (commute (F | {x})) . a = x .--> (fx . a) by A10, Th3;
then A11: rng ((commute (F | {x})) . a) = {(fx . a)} by FUNCOP_1:8;
assume S = rng ((commute (F | (B \/ {x}))) . a) ; :: thesis:
hence fx . a = max S by A11, A9, XXREAL_2:11; :: thesis:

end;

end;

suppose A12: B <> {} ; :: thesis:

then reconsider B9 = B as non empty set ;
consider f being continuous Function of X,R such that
A13: for x being Point of X
for S being non empty finite Subset of REAL st S = rng ((commute (F | B9)) . x) holds
f . x = max S by A8;
consider h being continuous Function of X,R such that
A14: for x being Point of X holds h . x = max ((f . x),(fx . x)) by Th50;
thus S₁[B \/ {x}] :: thesis:

proof

F is Function of A,(Funcs ( the carrier of X, the carrier of R)) by A4, FUNCT_2:66;
then F | B is Function of B,(Funcs ( the carrier of X, the carrier of R)) by A7, FUNCT_2:32;
then F | B in Funcs (B,(Funcs ( the carrier of X, the carrier of R))) by FUNCT_2:8;
then commute (F | B) in Funcs ( the carrier of X,(Funcs (B, the carrier of R))) by A12, FUNCT_6:55;
then reconsider cFB = commute (F | B) as Function of the carrier of X,(Funcs (B, the carrier of R)) by FUNCT_2:66;
assume not B \/ {x} is empty ; :: thesis:
take h ; :: thesis:
let a be Point of X; :: thesis:
let S be non empty finite Subset of REAL; :: thesis:
reconsider cFBa = cFB . a as Function of B9, the carrier of R ;
A15: dom fx = the carrier of X by FUNCT_2:def 1;
F | (B \/ {x}) = (F | B) \/ (F | {x}) by RELAT_1:78;
then A16: (commute (F | (B \/ {x}))) . a = (cFB . a) \/ ((commute (F | {x})) . a) by Th7;
assume S = rng ((commute (F | (B \/ {x}))) . a) ; :: thesis:
then A17: S = (rng cFBa) \/ (rng ((commute (F | {x})) . a)) by A16, RELAT_1:12;
then rng cFBa c= S by XBOOLE_1:7;
then reconsider S1 = rng cFBa as non empty finite Subset of REAL by XBOOLE_1:1;
F | {x} = x .--> (F . x) by A2, A6, FUNCT_7:6;
then (commute (F | {x})) . a = x .--> (fx . a) by A15, Th3;
then A18: S = S1 \/ {(fx . a)} by A17, FUNCOP_1:8;
f . a = max S1 by A13;
then max S = max ((f . a),(max {(fx . a)})) by A18, XXREAL_2:10
.= max ((f . a),(fx . a)) by XXREAL_2:11 ;
hence h . a = max S by A14; :: thesis:

end;

end;

end;

end;

A19: A is finite ;
S₁[A] from FINSET_1:sch 2(A19, A1, A5);
hence ex f being continuous Function of X,R st
for x being Point of X
for S being non empty finite Subset of REAL st S = rng ((commute F) . x) holds
f . x = max S ; :: thesis: