let x0 be Complex; :: thesis: for f1, f2 being PartFunc of COMPLEX,COMPLEX st f1 is_continuous_in x0 & f1 /. x0 <> 0 & f2 is_continuous_in x0 holds
f2 / f1 is_continuous_in x0
let f1, f2 be PartFunc of COMPLEX,COMPLEX; :: thesis: ( f1 is_continuous_in x0 & f1 /. x0 <> 0 & f2 is_continuous_in x0 implies f2 / f1 is_continuous_in x0 )
assume that
A1: ( f1 is_continuous_in x0 & f1 /. x0 <> 0 ) and
A2: f2 is_continuous_in x0 ; :: thesis: f2 / f1 is_continuous_in x0
f1 ^ is_continuous_in x0 by A1, Th36;
then f2 (#) (f1 ^) is_continuous_in x0 by A2, Th33;
hence f2 / f1 is_continuous_in x0 by CFUNCT_1:39; :: thesis: verum