let Z be open Subset of REAL; :: thesis: for A being non empty closed_interval Subset of REAL st not 0 in Z & A c= Z holds
((id Z) ^) | A is continuous
let A be non empty closed_interval Subset of REAL; :: thesis: ( not 0 in Z & A c= Z implies ((id Z) ^) | A is continuous )
assume A1: ( not 0 in Z & A c= Z ) ; :: thesis: ((id Z) ^) | A is continuous
then (id Z) ^ is_differentiable_on Z by FDIFF_5:4;
then ((id Z) ^) | Z is continuous by FDIFF_1:25;
hence ((id Z) ^) | A is continuous by A1, FCONT_1:16; :: thesis: verum