let n be Nat; :: thesis: for A being affinely-independent Subset of (TOP-REAL n) st card A = n + 1 holds
for f being continuous Function of ((TOP-REAL n) | (conv A)),((TOP-REAL n) | (conv A)) holds f is with_fixpoint
let A be affinely-independent Subset of (TOP-REAL n); :: thesis: ( card A = n + 1 implies for f being continuous Function of ((TOP-REAL n) | (conv A)),((TOP-REAL n) | (conv A)) holds f is with_fixpoint )
assume A1: card A = n + 1 ; :: thesis: for f being continuous Function of ((TOP-REAL n) | (conv A)),((TOP-REAL n) | (conv A)) holds f is with_fixpoint
let f be continuous Function of ((TOP-REAL n) | (conv A)),((TOP-REAL n) | (conv A)); :: thesis: f is with_fixpoint
consider x being Point of (TOP-REAL n) such that
A2: ( x in dom f & f . x = x ) by A1, Th23;
x is_a_fixpoint_of f by A2, ABIAN:def 3;
hence f is with_fixpoint by ABIAN:def 5; :: thesis: verum