let X be set ; :: thesis:
let CNS1, CNS2 be ComplexNormSpace; :: thesis:
let f be PartFunc of CNS1,CNS2; :: thesis:
assume A1: f is_uniformly_continuous_on X ; :: thesis:
then A2: ( X c= dom f & ( for r being Real st 0 < r holds
ex s being Real st
( 0 < s & ( for x1, x2 being Point of CNS1 st x1 in X & x2 in X & ||.(x1 - x2).|| < s holds
||.((f /. x1) - (f /. x2)).|| < r ) ) ) ) by Def1;

let x0 be Point of CNS1; :: thesis:
let r be Real; :: thesis:
assume A3: ( x0 in X & 0 < r ) ; :: thesis:
then consider s being Real such that
A4: ( 0 < s & ( for x1, x2 being Point of CNS1 st x1 in X & x2 in X & ||.(x1 - x2).|| < s holds
||.((f /. x1) - (f /. x2)).|| < r ) ) by A1, Def1;
take s = s; :: thesis:
thus 0 < s by A4; :: thesis:
let x1 be Point of CNS1; :: thesis:
assume ( x1 in X & ||.(x1 - x0).|| < s ) ; :: thesis:
hence ||.((f /. x1) - (f /. x0)).|| < r by A3, A4; :: thesis:

end;

hence f is_continuous_on X by A2, NCFCONT1:65; :: thesis: