let n be Nat; for A being convex Subset of (TOP-REAL n) st A is compact & not A is boundary holds
for h being continuous Function of ((TOP-REAL n) | A),((TOP-REAL n) | A) holds h is with_fixpoint
set T = TOP-REAL n;
consider I being affinely-independent Subset of (TOP-REAL n) such that
{} (TOP-REAL n) c= I
and
I c= [#] (TOP-REAL n)
and
A1:
Affin I = Affin ([#] (TOP-REAL n))
by RLAFFIN1:60;
reconsider TT = TOP-REAL n as non empty RLSStruct ;
reconsider i = I as Subset of TT ;
set II = Int i;
A2:
not I is empty
by A1;
then A3:
not Int i is empty
by RLAFFIN2:20;
reconsider ii = Int i as Subset of (TOP-REAL n) ;
A4:
Int ii c= Int (conv I)
by RLAFFIN2:5, TOPS_1:19;
let A be convex Subset of (TOP-REAL n); ( A is compact & not A is boundary implies for h being continuous Function of ((TOP-REAL n) | A),((TOP-REAL n) | A) holds h is with_fixpoint )
assume A5:
( A is compact & not A is boundary )
; for h being continuous Function of ((TOP-REAL n) | A),((TOP-REAL n) | A) holds h is with_fixpoint
A6:
not A is empty
by A5;
let h be continuous Function of ((TOP-REAL n) | A),((TOP-REAL n) | A); h is with_fixpoint
[#] (TOP-REAL n) is Affine
by RUSUB_4:22;
then
( dim (TOP-REAL n) = n & Affin ([#] (TOP-REAL n)) = [#] (TOP-REAL n) )
by RLAFFIN1:50, RLAFFIN3:4;
then A7:
card I = n + 1
by A1, RLAFFIN3:6;
then
ii is open
by RLAFFIN3:33;
then
not conv I is boundary
by A3, A4, TOPS_1:23;
then consider f being Function of ((TOP-REAL n) | A),((TOP-REAL n) | (conv I)) such that
A8:
f is being_homeomorphism
and
f .: (Fr A) = Fr (conv I)
by A5, Th7;
reconsider fhf = f * (h * (f ")) as Function of ((TOP-REAL n) | (conv I)),((TOP-REAL n) | (conv I)) by A6;
f " is continuous
by A8, TOPS_2:def 5;
then consider p being Point of (TOP-REAL n) such that
A9:
p in dom fhf
and
A10:
fhf . p = p
by A7, A2, A8, A6, SIMPLEX2:23;
A11:
p in dom (h * (f "))
by A9, FUNCT_1:11;
reconsider F = f as Function ;
A12:
rng f = [#] ((TOP-REAL n) | (conv I))
by A8, TOPS_2:def 5;
A13:
f " = F "
by A8, TOPS_2:def 4;
consider x being object such that
A14:
x in dom F
and
A15:
F . x = p
by A12, A9, FUNCT_1:def 3;
(F ") . p = x
by A8, A14, A15, FUNCT_1:34;
then
(h * (f ")) . p = h . x
by A11, A13, FUNCT_1:12;
then A16:
p = f . (h . x)
by A9, A10, FUNCT_1:12;
A17:
dom f = [#] ((TOP-REAL n) | A)
by A8, TOPS_2:def 5;
then A18:
x in dom h
by A14, FUNCT_2:52;
then
h . x in rng h
by FUNCT_1:def 3;
then
h . x = x
by A8, A17, A14, A15, A16, FUNCT_1:def 4;
then
x is_a_fixpoint_of h
by A18, ABIAN:def 3;
hence
h is with_fixpoint
by ABIAN:def 5; verum