begin
:: deftheorem Def1 defines is_uniformly_continuous_on NCFCONT2:def 1 :
:: deftheorem Def2 defines is_uniformly_continuous_on NCFCONT2:def 2 :
:: deftheorem Def3 defines is_uniformly_continuous_on NCFCONT2:def 3 :
:: deftheorem Def4 defines is_uniformly_continuous_on NCFCONT2:def 4 :
:: deftheorem Def5 defines is_uniformly_continuous_on NCFCONT2:def 5 :
:: deftheorem Def6 defines is_uniformly_continuous_on NCFCONT2:def 6 :
theorem Th1:
theorem Th2:
theorem Th3:
theorem
theorem
theorem
theorem
theorem
theorem
theorem Th10:
theorem Th11:
theorem Th12:
theorem
theorem
theorem
theorem
theorem
theorem
theorem Th19:
theorem Th20:
theorem Th21:
theorem
theorem Th23:
theorem
theorem Th25:
theorem Th26:
theorem Th27:
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
begin
:: deftheorem Def7 defines contraction NCFCONT2:def 7 :
theorem
theorem
Lm1:
for X being ComplexNormSpace
for x, y, z being Point of X
for e being Real st ||.(x - z).|| < e / 2 & ||.(z - y).|| < e / 2 holds
||.(x - y).|| < e
Lm2:
for X being ComplexNormSpace
for x, y, z being Point of X
for e being Real st ||.(x - z).|| < e / 2 & ||.(y - z).|| < e / 2 holds
||.(x - y).|| < e
Lm3:
for X being ComplexNormSpace
for x being Point of X st ( for e being Real st e > 0 holds
||.x.|| < e ) holds
x = 0. X
Lm4:
for X being ComplexNormSpace
for x, y being Point of X st ( for e being Real st e > 0 holds
||.(x - y).|| < e ) holds
x = y
theorem Th40:
theorem