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

for x being Real st x in Z holds

((#R (1 / 2)) `| Z) . x = (1 / 2) * (x #R (- (1 / 2)))

((#R (1 / 2)) `| Z) . x = (1 / 2) * (x #R (- (1 / 2))) ) ) by A1, A2, FDIFF_1:9; :: thesis: verum

((#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

then A3:
#R (1 / 2) is_differentiable_on Z
by A1, FDIFF_1:9;
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;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

for x being Real st x in Z holds

((#R (1 / 2)) `| Z) . x = (1 / 2) * (x #R (- (1 / 2)))

proof

hence
( #R (1 / 2) is_differentiable_on Z & ( for x being Real st x in Z holds
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;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

((#R (1 / 2)) `| Z) . x = (1 / 2) * (x #R (- (1 / 2))) ) ) by A1, A2, FDIFF_1:9; :: thesis: verum