let f1, f2 be PartFunc of REAL , REAL ; :: thesis: for x0 being Real st f1 is_left_differentiable_in x0 & f2 is_left_differentiable_in x0 & f2 . x0 <> 0 holds
( f1 / f2 is_left_differentiable_in x0 & Ldiff (f1 / f2),x0 = (((Ldiff f1,x0) * (f2 . x0)) - ((Ldiff f2,x0) * (f1 . x0))) / ((f2 . x0) ^2 ) )
let x0 be Real; :: thesis: ( f1 is_left_differentiable_in x0 & f2 is_left_differentiable_in x0 & f2 . x0 <> 0 implies ( f1 / f2 is_left_differentiable_in x0 & Ldiff (f1 / f2),x0 = (((Ldiff f1,x0) * (f2 . x0)) - ((Ldiff f2,x0) * (f1 . x0))) / ((f2 . x0) ^2 ) ) )
assume A1: ( f1 is_left_differentiable_in x0 & f2 is_left_differentiable_in x0 & f2 . x0 <> 0 ) ; :: thesis: ( f1 / f2 is_left_differentiable_in x0 & Ldiff (f1 / f2),x0 = (((Ldiff f1,x0) * (f2 . x0)) - ((Ldiff f2,x0) * (f1 . x0))) / ((f2 . x0) ^2 ) )
then A2: f2 is_Lcontinuous_in x0 by Th5;
ex r being Real st
( r > 0 & [.(x0 - r),x0.] c= dom f2 ) by A1, Def4;
then consider r1 being Real such that
A3: ( r1 > 0 & [.(x0 - r1),x0.] c= dom f2 & ( for g being Real st g in [.(x0 - r1),x0.] holds
f2 . g <> 0 ) ) by A1, A2, Th6;

now

take r1 = r1; :: thesis: ( r1 > 0 & ( for g being Real st g in dom f2 & g in [.(x0 - r1),x0.] holds
f2 . g <> 0 ) )
thus r1 > 0 by A3; :: thesis: for g being Real st g in dom f2 & g in [.(x0 - r1),x0.] holds
f2 . g <> 0
let g be Real; :: thesis: ( g in dom f2 & g in [.(x0 - r1),x0.] implies f2 . g <> 0 )
assume ( g in dom f2 & g in [.(x0 - r1),x0.] ) ; :: thesis: f2 . g <> 0
hence f2 . g <> 0 by A3; :: thesis: verum

end;

hence ( f1 / f2 is_left_differentiable_in x0 & Ldiff (f1 / f2),x0 = (((Ldiff f1,x0) * (f2 . x0)) - ((Ldiff f2,x0) * (f1 . x0))) / ((f2 . x0) ^2 ) ) by A1, Lm1; :: thesis: verum