let X be set ; :: thesis: for f1, f2 being PartFunc of COMPLEX,COMPLEX st f1 is_continuous_on X & f1 " {0} = {} & f2 is_continuous_on X holds
f2 / f1 is_continuous_on X
let f1, f2 be PartFunc of COMPLEX,COMPLEX; :: thesis: ( f1 is_continuous_on X & f1 " {0} = {} & f2 is_continuous_on X implies f2 / f1 is_continuous_on X )
assume that
A1: ( f1 is_continuous_on X & f1 " {0} = {} ) and
A2: f2 is_continuous_on X ; :: thesis: f2 / f1 is_continuous_on X
f1 ^ is_continuous_on X by A1, Th47;
then f2 (#) (f1 ^) is_continuous_on X by A2, Th43;
hence f2 / f1 is_continuous_on X by CFUNCT_1:39; :: thesis: verum