:: ALI2 semantic presentation

definition
let c1 be non empty MetrSpace;
mode contraction of c1 -> Function of a1,a1 means :Def1: :: ALI2:def 1
ex b1 being Real st
( 0 < b1 & b1 < 1 & ( for b2, b3 being Point of a1 holds dist (a2 . b2),(a2 . b3) <= b1 * (dist b2,b3) ) );
existence
ex b1 being Function of c1,c1ex b2 being Real st
( 0 < b2 & b2 < 1 & ( for b3, b4 being Point of c1 holds dist (b1 . b3),(b1 . b4) <= b2 * (dist b3,b4) ) )
proof end;
end;

:: deftheorem Def1 defines contraction ALI2:def 1 :
for b1 being non empty MetrSpace
for b2 being Function of b1,b1 holds
( b2 is contraction of b1 iff ex b3 being Real st
( 0 < b3 & b3 < 1 & ( for b4, b5 being Point of b1 holds dist (b2 . b4),(b2 . b5) <= b3 * (dist b4,b5) ) ) );

theorem Th1: :: ALI2:1
canceled;

theorem Th2: :: ALI2:2
for b1 being non empty MetrSpace
for b2 being contraction of b1 st TopSpaceMetr b1 is compact holds
ex b3 being Point of b1 st
( b2 . b3 = b3 & ( for b4 being Point of b1 st b2 . b4 = b4 holds
b4 = b3 ) )
proof end;