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, Th69;
then f2 (#) (f1 ^ ) is_continuous_on X by A2, Th65;
hence f2 / f1 is_continuous_on X by CFUNCT_1:51; :: thesis: verum