let X be set ; :: thesis: for f being PartFunc of COMPLEX,COMPLEX st f is_continuous_on X & (f | X) " {0} = {} holds
f ^ is_continuous_on X
let f be PartFunc of COMPLEX,COMPLEX; :: thesis: ( f is_continuous_on X & (f | X) " {0} = {} implies f ^ is_continuous_on X )
assume that
A1: f is_continuous_on X and
A2: (f | X) " {0} = {} ; :: thesis: f ^ is_continuous_on X
f | X is_continuous_on X by A1, Th40;
then (f | X) ^ is_continuous_on X by A2, Th47;
then (f ^) | X is_continuous_on X by CFUNCT_1:54;
hence f ^ is_continuous_on X by Th40; :: thesis: verum