let x be Element of COMPLEX ; :: thesis: COMPLEX --> x is_continuous_on COMPLEX
A1: dom (COMPLEX --> x) = COMPLEX by FUNCOP_1:19;

now

let x1 be Element of COMPLEX ; :: thesis: for r being Real st x1 in COMPLEX & 0 < r holds
ex s being Real st
( 0 < s & ( for x2 being Element of 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 Element of COMPLEX st x2 in COMPLEX & |.(x2 - x1).| < s holds
|.(((COMPLEX --> x) /. x2) - ((COMPLEX --> x) /. x1)).| < r ) ) )
assume that
x1 in COMPLEX and
A2: 0 < r ; :: thesis: ex s being Real st
( 0 < s & ( for x2 being Element of 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 Element of COMPLEX st x2 in COMPLEX & |.(x2 - x1).| < s holds
|.(((COMPLEX --> x) /. x2) - ((COMPLEX --> x) /. x1)).| < r ) )
thus 0 < s by A2; :: thesis: for x2 being Element of COMPLEX st x2 in COMPLEX & |.(x2 - x1).| < s holds
|.(((COMPLEX --> x) /. x2) - ((COMPLEX --> x) /. x1)).| < r
let x2 be Element of COMPLEX ; :: thesis: ( x2 in COMPLEX & |.(x2 - x1).| < s implies |.(((COMPLEX --> x) /. x2) - ((COMPLEX --> x) /. x1)).| < r )
assume that
x2 in COMPLEX and
|.(x2 - x1).| < s ; :: thesis: |.(((COMPLEX --> x) /. x2) - ((COMPLEX --> x) /. x1)).| < r
A3: (COMPLEX --> x) /. x1 = x by FUNCOP_1:13;
(COMPLEX --> x) /. x2 = x by FUNCOP_1:13;
hence |.(((COMPLEX --> x) /. x2) - ((COMPLEX --> x) /. x1)).| < r by A2, A3, COMPLEX1:130; :: thesis: verum

end;

hence COMPLEX --> x is_continuous_on COMPLEX by A1, CFCONT_1:61; :: thesis: verum