let Z be open Subset of REAL; :: thesis: ( Z c= dom (#R (1 / 2)) implies ( #R (1 / 2) is_differentiable_on Z & ( for x being Real st x in Z holds
((#R (1 / 2)) `| Z) . x = (1 / 2) * (x #R (- (1 / 2))) ) ) )
assume A1: Z c= dom (#R (1 / 2)) ; :: thesis: ( #R (1 / 2) is_differentiable_on Z & ( for x being Real st x in Z holds
((#R (1 / 2)) `| Z) . x = (1 / 2) * (x #R (- (1 / 2))) ) )
A2: for x being Real st x in Z holds
#R (1 / 2) is_differentiable_in x

proof

let x be Real; :: thesis: ( x in Z implies #R (1 / 2) is_differentiable_in x )
assume x in Z ; :: thesis: #R (1 / 2) is_differentiable_in x
then x in dom (#R (1 / 2)) by A1;
then x in right_open_halfline 0 by TAYLOR_1:def 4;
then x > 0 by XXREAL_1:4;
hence #R (1 / 2) is_differentiable_in x by TAYLOR_1:21; :: thesis: verum

end;

then A3: #R (1 / 2) is_differentiable_on Z by A1, FDIFF_1:9;
for x being Real st x in Z holds
((#R (1 / 2)) `| Z) . x = (1 / 2) * (x #R (- (1 / 2)))

proof

let x be Real; :: thesis: ( x in Z implies ((#R (1 / 2)) `| Z) . x = (1 / 2) * (x #R (- (1 / 2))) )
assume A4: x in Z ; :: thesis: ((#R (1 / 2)) `| Z) . x = (1 / 2) * (x #R (- (1 / 2)))
then x in dom (#R (1 / 2)) by A1;
then x in right_open_halfline 0 by TAYLOR_1:def 4;
then x > 0 by XXREAL_1:4;
then diff ((#R (1 / 2)),x) = (1 / 2) * (x #R ((1 / 2) - 1)) by TAYLOR_1:21
.= (1 / 2) * (x #R (- (1 / 2))) ;
hence ((#R (1 / 2)) `| Z) . x = (1 / 2) * (x #R (- (1 / 2))) by A3, A4, FDIFF_1:def 7; :: thesis: verum

end;

hence ( #R (1 / 2) is_differentiable_on Z & ( for x being Real st x in Z holds
((#R (1 / 2)) `| Z) . x = (1 / 2) * (x #R (- (1 / 2))) ) ) by A1, A2, FDIFF_1:9; :: thesis: verum