let x be Element of COMPLEX ; :: thesis: COMPLEX --> x is_continuous_on COMPLEX

A1: now :: thesis: for x1 being Complex
for r being Real st x1 in COMPLEX & 0 < r holds
ex s being Real st
( 0 < s & ( for x2 being Complex st x2 in COMPLEX & |.(x2 - x1).| < s holds
|.(((COMPLEX --> x) /. x2) - ((COMPLEX --> x) /. x1)).| < r ) )

let x1 be Complex; :: thesis: for r being Real st x1 in COMPLEX & 0 < r holds
ex s being Real st
( 0 < s & ( for x2 being Complex st x2 in COMPLEX & |.(x2 - x1).| < s holds
|.(((COMPLEX --> x) /. x2) - ((COMPLEX --> x) /. x1)).| < r ) )
let r be Real; :: thesis: ( x1 in COMPLEX & 0 < r implies ex s being Real st
( 0 < s & ( for x2 being Complex st x2 in COMPLEX & |.(x2 - x1).| < s holds
|.(((COMPLEX --> x) /. x2) - ((COMPLEX --> x) /. x1)).| < r ) ) )
assume that
A2: x1 in COMPLEX and
A3: 0 < r ; :: thesis: ex s being Real st
( 0 < s & ( for x2 being Complex st x2 in COMPLEX & |.(x2 - x1).| < s holds
|.(((COMPLEX --> x) /. x2) - ((COMPLEX --> x) /. x1)).| < r ) )
take s = r; :: thesis: ( 0 < s & ( for x2 being Complex st x2 in COMPLEX & |.(x2 - x1).| < s holds
|.(((COMPLEX --> x) /. x2) - ((COMPLEX --> x) /. x1)).| < r ) )
thus 0 < s by A3; :: thesis: for x2 being Complex st x2 in COMPLEX & |.(x2 - x1).| < s holds
|.(((COMPLEX --> x) /. x2) - ((COMPLEX --> x) /. x1)).| < r
let x2 be Complex; :: thesis: ( x2 in COMPLEX & |.(x2 - x1).| < s implies |.(((COMPLEX --> x) /. x2) - ((COMPLEX --> x) /. x1)).| < r )
assume that
A4: x2 in COMPLEX and
|.(x2 - x1).| < s ; :: thesis: |.(((COMPLEX --> x) /. x2) - ((COMPLEX --> x) /. x1)).| < r
reconsider xx1 = x1, xx2 = x2 as Element of COMPLEX by A2, A4;
( (COMPLEX --> x) /. xx1 = x & (COMPLEX --> x) /. xx2 = x ) by FUNCOP_1:7;
hence |.(((COMPLEX --> x) /. x2) - ((COMPLEX --> x) /. x1)).| < r by A3, COMPLEX1:44; :: thesis: verum

end;

dom (COMPLEX --> x) = COMPLEX by FUNCOP_1:13;
hence COMPLEX --> x is_continuous_on COMPLEX by A1, CFCONT_1:39; :: thesis: verum