A1: now

let x be Element of COMPLEX ; :: thesis: for r being Real st x in COMPLEX & 0 < r holds
ex s being Real st
( 0 < s & ( for y being Element of 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 Element of 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 Element of 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 Element of 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 Element of COMPLEX st y in COMPLEX & |.(y - x).| < s holds
|.(((id COMPLEX) /. y) - ((id COMPLEX) /. x)).| < r
let y be Element of 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
(id COMPLEX) /. x = x by FUNCT_1:35;
hence |.(((id COMPLEX) /. y) - ((id COMPLEX) /. x)).| < r by A3, FUNCT_1:35; :: thesis: verum

end;

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