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

let x be Complex; :: thesis: for r being Real st x in COMPLEX & 0 < r holds
ex s being Real st
( 0 < s & ( for y being Complex st y in COMPLEX & |.(y - x).| < s holds
|.(((id COMPLEX) /. y) - ((id COMPLEX) /. x)).| < r ) )
let r be Real; :: thesis: ( x in COMPLEX & 0 < r implies ex s being Real st
( 0 < s & ( for y being Complex st y in COMPLEX & |.(y - x).| < s holds
|.(((id COMPLEX) /. y) - ((id COMPLEX) /. x)).| < r ) ) )
assume that
x in COMPLEX and
A2: 0 < r ; :: thesis: ex s being Real st
( 0 < s & ( for y being Complex st y in COMPLEX & |.(y - x).| < s holds
|.(((id COMPLEX) /. y) - ((id COMPLEX) /. x)).| < r ) )
take s = r; :: thesis: ( 0 < s & ( for y being Complex st y in COMPLEX & |.(y - x).| < s holds
|.(((id COMPLEX) /. y) - ((id COMPLEX) /. x)).| < r ) )
thus 0 < s by A2; :: thesis: for y being Complex st y in COMPLEX & |.(y - x).| < s holds
|.(((id COMPLEX) /. y) - ((id COMPLEX) /. x)).| < r
let y be Complex; :: thesis: ( y in COMPLEX & |.(y - x).| < s implies |.(((id COMPLEX) /. y) - ((id COMPLEX) /. x)).| < r )
assume that
y in COMPLEX and
A3: |.(y - x).| < s ; :: thesis: |.(((id COMPLEX) /. y) - ((id COMPLEX) /. x)).| < r
reconsider xx = x, yy = y as Element of COMPLEX by XCMPLX_0:def 2;
|.(((id COMPLEX) /. yy) - ((id COMPLEX) /. xx)).| < r by A3;
hence |.(((id COMPLEX) /. y) - ((id COMPLEX) /. x)).| < r ; :: thesis: verum

end;

dom (id COMPLEX) = COMPLEX by FUNCT_2:def 1;
hence id COMPLEX is_continuous_on COMPLEX by A1, CFCONT_1:39; :: thesis: verum