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, Th62;
then (f | X) ^ is_continuous_on X by A2, Th69;
then (f ^ ) | X is_continuous_on X by CFUNCT_1:66;
hence f ^ is_continuous_on X by Th62; :: thesis: verum