:: FDIFF_6 semantic presentation

Lemma1: for b1 being Real holds 1 - (cos (2 * b1)) = 2 * ((sin b1) ^2 )
proof end;

Lemma2: for b1 being Real holds 1 + (cos (2 * b1)) = 2 * ((cos b1) ^2 )
proof end;

Lemma3: for b1 being Real st sin . b1 > 0 holds
sin . b1 = ((1 - (cos . b1)) * (1 + (cos . b1))) #R (1 / 2)
proof end;

Lemma4: for b1 being Real st sin . b1 > 0 & cos . b1 < 1 & cos . b1 > - 1 holds
(sin . b1) / ((1 - (cos . b1)) #R (1 / 2)) = (1 + (cos . b1)) #R (1 / 2)
proof end;

theorem Th1: :: FDIFF_6:1
for b1, b2 being Real st b1 > 0 holds
exp . (b2 * (log number_e ,b1)) = b1 #R b2
proof end;

theorem Th2: :: FDIFF_6:2
for b1, b2 being Real st b1 > 0 holds
exp . (- (b2 * (log number_e ,b1))) = b1 #R (- b2)
proof end;

Lemma7: for b1 being Real st sin . b1 > 0 & cos . b1 < 1 & cos . b1 > - 1 holds
(sin . b1) / ((1 + (cos . b1)) #R (1 / 2)) = (1 - (cos . b1)) #R (1 / 2)
proof end;

theorem Th3: :: FDIFF_6:3
for b1 being Real
for b2 being open Subset of REAL
for b3, b4 being PartFunc of REAL , REAL st b2 c= dom (b3 - b4) & ( for b5 being Real st b5 in b2 holds
b3 . b5 = b1 ^2 ) & b4 = #Z 2 holds
( b3 - b4 is_differentiable_on b2 & ( for b5 being Real st b5 in b2 holds
((b3 - b4) `| b2) . b5 = - (2 * b5) ) )
proof end;

theorem Th4: :: FDIFF_6:4
for b1 being Real
for b2 being open Subset of REAL
for b3, b4 being PartFunc of REAL , REAL st b2 c= dom ((b3 + b4) / (b3 - b4)) & b4 = #Z 2 & ( for b5 being Real st b5 in b2 holds
( b3 . b5 = b1 ^2 & (b3 - b4) . b5 <> 0 ) ) holds
( (b3 + b4) / (b3 - b4) is_differentiable_on b2 & ( for b5 being Real st b5 in b2 holds
(((b3 + b4) / (b3 - b4)) `| b2) . b5 = ((4 * (b1 ^2 )) * b5) / (((b1 ^2 ) - (b5 |^ 2)) ^2 ) ) )
proof end;

theorem Th5: :: FDIFF_6:5
for b1 being Real
for b2 being open Subset of REAL
for b3, b4, b5 being PartFunc of REAL , REAL st b2 c= dom b3 & b3 = (log_ number_e ) * ((b4 + b5) / (b4 - b5)) & b5 = #Z 2 & ( for b6 being Real st b6 in b2 holds
( b4 . b6 = b1 ^2 & (b4 - b5) . b6 > 0 & b1 <> 0 ) ) holds
( b3 is_differentiable_on b2 & ( for b6 being Real st b6 in b2 holds
(b3 `| b2) . b6 = ((4 * (b1 ^2 )) * b6) / ((b1 |^ 4) - (b6 |^ 4)) ) )
proof end;

theorem Th6: :: FDIFF_6:6
for b1 being Real
for b2 being open Subset of REAL
for b3, b4, b5 being PartFunc of REAL , REAL st b2 c= dom ((1 / (4 * (b1 ^2 ))) (#) b3) & b3 = (log_ number_e ) * ((b4 + b5) / (b4 - b5)) & b5 = #Z 2 & ( for b6 being Real st b6 in b2 holds
( b4 . b6 = b1 ^2 & (b4 - b5) . b6 > 0 & b1 <> 0 ) ) holds
( (1 / (4 * (b1 ^2 ))) (#) b3 is_differentiable_on b2 & ( for b6 being Real st b6 in b2 holds
(((1 / (4 * (b1 ^2 ))) (#) b3) `| b2) . b6 = b6 / ((b1 |^ 4) - (b6 |^ 4)) ) )
proof end;

theorem Th7: :: FDIFF_6:7
for b1 being open Subset of REAL
for b2, b3 being PartFunc of REAL , REAL st b1 c= dom (b2 / (b3 + b2)) & b2 = #Z 2 & ( for b4 being Real st b4 in b1 holds
( b3 . b4 = 1 & b4 <> 0 ) ) holds
( b2 / (b3 + b2) is_differentiable_on b1 & ( for b4 being Real st b4 in b1 holds
((b2 / (b3 + b2)) `| b1) . b4 = (2 * b4) / ((1 + (b4 ^2 )) ^2 ) ) )
proof end;

theorem Th8: :: FDIFF_6:8
for b1 being open Subset of REAL
for b2, b3, b4 being PartFunc of REAL , REAL st b1 c= dom ((1 / 2) (#) b2) & b2 = (log_ number_e ) * (b3 / (b4 + b3)) & b3 = #Z 2 & ( for b5 being Real st b5 in b1 holds
( b4 . b5 = 1 & b5 <> 0 ) ) holds
( (1 / 2) (#) b2 is_differentiable_on b1 & ( for b5 being Real st b5 in b1 holds
(((1 / 2) (#) b2) `| b1) . b5 = 1 / (b5 * (1 + (b5 ^2 ))) ) )
proof end;

theorem Th9: :: FDIFF_6:9
for b1 being Nat
for b2 being open Subset of REAL st b2 c= dom ((log_ number_e ) * (#Z b1)) & ( for b3 being Real st b3 in b2 holds
b3 > 0 ) holds
( (log_ number_e ) * (#Z b1) is_differentiable_on b2 & ( for b3 being Real st b3 in b2 holds
(((log_ number_e ) * (#Z b1)) `| b2) . b3 = b1 / b3 ) )
proof end;

theorem Th10: :: FDIFF_6:10
for b1 being open Subset of REAL
for b2, b3 being PartFunc of REAL , REAL st b1 c= dom ((b2 ^ ) + ((log_ number_e ) * (b3 / b2))) & ( for b4 being Real st b4 in b1 holds
( b2 . b4 = b4 & b2 . b4 > 0 & b3 . b4 = b4 - 1 & b3 . b4 > 0 ) ) holds
( (b2 ^ ) + ((log_ number_e ) * (b3 / b2)) is_differentiable_on b1 & ( for b4 being Real st b4 in b1 holds
(((b2 ^ ) + ((log_ number_e ) * (b3 / b2))) `| b1) . b4 = 1 / ((b4 ^2 ) * (b4 - 1)) ) )
proof end;

theorem Th11: :: FDIFF_6:11
for b1 being Real
for b2 being open Subset of REAL
for b3 being PartFunc of REAL , REAL st b2 c= dom (exp * b3) & ( for b4 being Real st b4 in b2 holds
b3 . b4 = b4 * (log number_e ,b1) ) & b1 > 0 holds
( exp * b3 is_differentiable_on b2 & ( for b4 being Real st b4 in b2 holds
((exp * b3) `| b2) . b4 = (b1 #R b4) * (log number_e ,b1) ) )
proof end;

theorem Th12: :: FDIFF_6:12
for b1 being Real
for b2 being open Subset of REAL
for b3, b4 being PartFunc of REAL , REAL st b2 c= dom ((1 / (log number_e ,b1)) (#) ((exp * b3) (#) b4)) & ( for b5 being Real st b5 in b2 holds
( b3 . b5 = b5 * (log number_e ,b1) & b4 . b5 = b5 - (1 / (log number_e ,b1)) ) ) & b1 > 0 & b1 <> 1 holds
( (1 / (log number_e ,b1)) (#) ((exp * b3) (#) b4) is_differentiable_on b2 & ( for b5 being Real st b5 in b2 holds
(((1 / (log number_e ,b1)) (#) ((exp * b3) (#) b4)) `| b2) . b5 = b5 * (b1 #R b5) ) )
proof end;

theorem Th13: :: FDIFF_6:13
for b1 being Real
for b2 being open Subset of REAL
for b3 being PartFunc of REAL , REAL st b2 c= dom ((1 / (1 + (log number_e ,b1))) (#) ((exp * b3) (#) exp )) & ( for b4 being Real st b4 in b2 holds
b3 . b4 = b4 * (log number_e ,b1) ) & b1 > 0 & b1 <> 1 / number_e holds
( (1 / (1 + (log number_e ,b1))) (#) ((exp * b3) (#) exp ) is_differentiable_on b2 & ( for b4 being Real st b4 in b2 holds
(((1 / (1 + (log number_e ,b1))) (#) ((exp * b3) (#) exp )) `| b2) . b4 = (b1 #R b4) * (exp . b4) ) )
proof end;

theorem Th14: :: FDIFF_6:14
for b1 being open Subset of REAL
for b2 being PartFunc of REAL , REAL st b1 c= dom (exp * b2) & ( for b3 being Real st b3 in b1 holds
b2 . b3 = - b3 ) holds
( exp * b2 is_differentiable_on b1 & ( for b3 being Real st b3 in b1 holds
((exp * b2) `| b1) . b3 = - (exp (- b3)) ) )
proof end;

theorem Th15: :: FDIFF_6:15
for b1 being open Subset of REAL
for b2, b3 being PartFunc of REAL , REAL st b1 c= dom (b2 (#) (exp * b3)) & ( for b4 being Real st b4 in b1 holds
( b2 . b4 = (- b4) - 1 & b3 . b4 = - b4 ) ) holds
( b2 (#) (exp * b3) is_differentiable_on b1 & ( for b4 being Real st b4 in b1 holds
((b2 (#) (exp * b3)) `| b1) . b4 = b4 / (exp b4) ) )
proof end;

theorem Th16: :: FDIFF_6:16
for b1 being Real
for b2 being open Subset of REAL
for b3 being PartFunc of REAL , REAL st b2 c= dom (- (exp * b3)) & ( for b4 being Real st b4 in b2 holds
b3 . b4 = - (b4 * (log number_e ,b1)) ) & b1 > 0 holds
( - (exp * b3) is_differentiable_on b2 & ( for b4 being Real st b4 in b2 holds
((- (exp * b3)) `| b2) . b4 = (b1 #R (- b4)) * (log number_e ,b1) ) )
proof end;

theorem Th17: :: FDIFF_6:17
for b1 being Real
for b2 being open Subset of REAL
for b3, b4 being PartFunc of REAL , REAL st b2 c= dom ((1 / (log number_e ,b1)) (#) ((- (exp * b3)) (#) b4)) & ( for b5 being Real st b5 in b2 holds
( b3 . b5 = - (b5 * (log number_e ,b1)) & b4 . b5 = b5 + (1 / (log number_e ,b1)) ) ) & b1 > 0 & b1 <> 1 holds
( (1 / (log number_e ,b1)) (#) ((- (exp * b3)) (#) b4) is_differentiable_on b2 & ( for b5 being Real st b5 in b2 holds
(((1 / (log number_e ,b1)) (#) ((- (exp * b3)) (#) b4)) `| b2) . b5 = b5 / (b1 #R b5) ) )
proof end;

theorem Th18: :: FDIFF_6:18
for b1 being Real
for b2 being open Subset of REAL
for b3 being PartFunc of REAL , REAL st b2 c= dom ((1 / ((log number_e ,b1) - 1)) (#) ((exp * b3) / exp )) & ( for b4 being Real st b4 in b2 holds
b3 . b4 = b4 * (log number_e ,b1) ) & b1 > 0 & b1 <> number_e holds
( (1 / ((log number_e ,b1) - 1)) (#) ((exp * b3) / exp ) is_differentiable_on b2 & ( for b4 being Real st b4 in b2 holds
(((1 / ((log number_e ,b1) - 1)) (#) ((exp * b3) / exp )) `| b2) . b4 = (b1 #R b4) / (exp . b4) ) )
proof end;

theorem Th19: :: FDIFF_6:19
for b1 being Real
for b2 being open Subset of REAL
for b3 being PartFunc of REAL , REAL st b2 c= dom ((1 / (1 - (log number_e ,b1))) (#) (exp / (exp * b3))) & ( for b4 being Real st b4 in b2 holds
b3 . b4 = b4 * (log number_e ,b1) ) & b1 > 0 & b1 <> number_e holds
( (1 / (1 - (log number_e ,b1))) (#) (exp / (exp * b3)) is_differentiable_on b2 & ( for b4 being Real st b4 in b2 holds
(((1 / (1 - (log number_e ,b1))) (#) (exp / (exp * b3))) `| b2) . b4 = (exp . b4) / (b1 #R b4) ) )
proof end;

theorem Th20: :: FDIFF_6:20
for b1 being open Subset of REAL
for b2 being PartFunc of REAL , REAL st b1 c= dom ((log_ number_e ) * (exp + b2)) & ( for b3 being Real st b3 in b1 holds
b2 . b3 = 1 ) holds
( (log_ number_e ) * (exp + b2) is_differentiable_on b1 & ( for b3 being Real st b3 in b1 holds
(((log_ number_e ) * (exp + b2)) `| b1) . b3 = (exp . b3) / ((exp . b3) + 1) ) )
proof end;

theorem Th21: :: FDIFF_6:21
for b1 being open Subset of REAL
for b2 being PartFunc of REAL , REAL st b1 c= dom ((log_ number_e ) * (exp - b2)) & ( for b3 being Real st b3 in b1 holds
( b2 . b3 = 1 & (exp - b2) . b3 > 0 ) ) holds
( (log_ number_e ) * (exp - b2) is_differentiable_on b1 & ( for b3 being Real st b3 in b1 holds
(((log_ number_e ) * (exp - b2)) `| b1) . b3 = (exp . b3) / ((exp . b3) - 1) ) )
proof end;

theorem Th22: :: FDIFF_6:22
for b1 being open Subset of REAL
for b2 being PartFunc of REAL , REAL st b1 c= dom (- ((log_ number_e ) * (b2 - exp ))) & ( for b3 being Real st b3 in b1 holds
( b2 . b3 = 1 & (b2 - exp ) . b3 > 0 ) ) holds
( - ((log_ number_e ) * (b2 - exp )) is_differentiable_on b1 & ( for b3 being Real st b3 in b1 holds
((- ((log_ number_e ) * (b2 - exp ))) `| b1) . b3 = (exp . b3) / (1 - (exp . b3)) ) )
proof end;

theorem Th23: :: FDIFF_6:23
for b1 being open Subset of REAL
for b2 being PartFunc of REAL , REAL st b1 c= dom (((#Z 2) * exp ) + b2) & ( for b3 being Real st b3 in b1 holds
b2 . b3 = 1 ) holds
( ((#Z 2) * exp ) + b2 is_differentiable_on b1 & ( for b3 being Real st b3 in b1 holds
((((#Z 2) * exp ) + b2) `| b1) . b3 = 2 * (exp (2 * b3)) ) )
proof end;

theorem Th24: :: FDIFF_6:24
for b1 being open Subset of REAL
for b2, b3 being PartFunc of REAL , REAL st b1 c= dom ((1 / 2) (#) ((log_ number_e ) * b2)) & b2 = ((#Z 2) * exp ) + b3 & ( for b4 being Real st b4 in b1 holds
b3 . b4 = 1 ) holds
( (1 / 2) (#) ((log_ number_e ) * b2) is_differentiable_on b1 & ( for b4 being Real st b4 in b1 holds
(((1 / 2) (#) ((log_ number_e ) * b2)) `| b1) . b4 = (exp b4) / ((exp b4) + (exp (- b4))) ) )
proof end;

theorem Th25: :: FDIFF_6:25
for b1 being open Subset of REAL
for b2 being PartFunc of REAL , REAL st b1 c= dom (((#Z 2) * exp ) - b2) & ( for b3 being Real st b3 in b1 holds
b2 . b3 = 1 ) holds
( ((#Z 2) * exp ) - b2 is_differentiable_on b1 & ( for b3 being Real st b3 in b1 holds
((((#Z 2) * exp ) - b2) `| b1) . b3 = 2 * (exp (2 * b3)) ) )
proof end;

theorem Th26: :: FDIFF_6:26
for b1 being open Subset of REAL
for b2, b3 being PartFunc of REAL , REAL st b1 c= dom ((1 / 2) (#) ((log_ number_e ) * b2)) & b2 = ((#Z 2) * exp ) - b3 & ( for b4 being Real st b4 in b1 holds
( b3 . b4 = 1 & b2 . b4 > 0 ) ) holds
( (1 / 2) (#) ((log_ number_e ) * b2) is_differentiable_on b1 & ( for b4 being Real st b4 in b1 holds
(((1 / 2) (#) ((log_ number_e ) * b2)) `| b1) . b4 = (exp b4) / ((exp b4) - (exp (- b4))) ) )
proof end;

theorem Th27: :: FDIFF_6:27
for b1 being open Subset of REAL
for b2 being PartFunc of REAL , REAL st b1 c= dom ((#Z 2) * (exp - b2)) & ( for b3 being Real st b3 in b1 holds
b2 . b3 = 1 ) holds
( (#Z 2) * (exp - b2) is_differentiable_on b1 & ( for b3 being Real st b3 in b1 holds
(((#Z 2) * (exp - b2)) `| b1) . b3 = (2 * (exp . b3)) * ((exp . b3) - 1) ) )
proof end;

theorem Th28: :: FDIFF_6:28
for b1 being open Subset of REAL
for b2, b3 being PartFunc of REAL , REAL st b1 c= dom b2 & b2 = (log_ number_e ) * (((#Z 2) * (exp - b3)) / exp ) & ( for b4 being Real st b4 in b1 holds
( b3 . b4 = 1 & (exp - b3) . b4 > 0 ) ) holds
( b2 is_differentiable_on b1 & ( for b4 being Real st b4 in b1 holds
(b2 `| b1) . b4 = ((exp . b4) + 1) / ((exp . b4) - 1) ) )
proof end;

theorem Th29: :: FDIFF_6:29
for b1 being open Subset of REAL
for b2 being PartFunc of REAL , REAL st b1 c= dom ((#Z 2) * (exp + b2)) & ( for b3 being Real st b3 in b1 holds
b2 . b3 = 1 ) holds
( (#Z 2) * (exp + b2) is_differentiable_on b1 & ( for b3 being Real st b3 in b1 holds
(((#Z 2) * (exp + b2)) `| b1) . b3 = (2 * (exp . b3)) * ((exp . b3) + 1) ) )
proof end;

theorem Th30: :: FDIFF_6:30
for b1 being open Subset of REAL
for b2, b3 being PartFunc of REAL , REAL st b1 c= dom b2 & b2 = (log_ number_e ) * (((#Z 2) * (exp + b3)) / exp ) & ( for b4 being Real st b4 in b1 holds
b3 . b4 = 1 ) holds
( b2 is_differentiable_on b1 & ( for b4 being Real st b4 in b1 holds
(b2 `| b1) . b4 = ((exp . b4) - 1) / ((exp . b4) + 1) ) )
proof end;

theorem Th31: :: FDIFF_6:31
for b1 being open Subset of REAL
for b2 being PartFunc of REAL , REAL st b1 c= dom ((#Z 2) * (b2 - exp )) & ( for b3 being Real st b3 in b1 holds
b2 . b3 = 1 ) holds
( (#Z 2) * (b2 - exp ) is_differentiable_on b1 & ( for b3 being Real st b3 in b1 holds
(((#Z 2) * (b2 - exp )) `| b1) . b3 = - ((2 * (exp . b3)) * (1 - (exp . b3))) ) )
proof end;

theorem Th32: :: FDIFF_6:32
for b1 being open Subset of REAL
for b2, b3 being PartFunc of REAL , REAL st b1 c= dom b2 & b2 = (log_ number_e ) * (exp / ((#Z 2) * (b3 - exp ))) & ( for b4 being Real st b4 in b1 holds
( b3 . b4 = 1 & (b3 - exp ) . b4 > 0 ) ) holds
( b2 is_differentiable_on b1 & ( for b4 being Real st b4 in b1 holds
(b2 `| b1) . b4 = (1 + (exp . b4)) / (1 - (exp . b4)) ) )
proof end;

theorem Th33: :: FDIFF_6:33
for b1 being open Subset of REAL
for b2, b3 being PartFunc of REAL , REAL st b1 c= dom b2 & b2 = (log_ number_e ) * (exp / ((#Z 2) * (b3 + exp ))) & ( for b4 being Real st b4 in b1 holds
b3 . b4 = 1 ) holds
( b2 is_differentiable_on b1 & ( for b4 being Real st b4 in b1 holds
(b2 `| b1) . b4 = (1 - (exp . b4)) / (1 + (exp . b4)) ) )
proof end;

theorem Th34: :: FDIFF_6:34
for b1 being open Subset of REAL
for b2, b3 being PartFunc of REAL , REAL st b1 c= dom ((log_ number_e ) * b2) & b2 = exp + (exp * b3) & ( for b4 being Real st b4 in b1 holds
b3 . b4 = - b4 ) holds
( (log_ number_e ) * b2 is_differentiable_on b1 & ( for b4 being Real st b4 in b1 holds
(((log_ number_e ) * b2) `| b1) . b4 = ((exp b4) - (exp (- b4))) / ((exp b4) + (exp (- b4))) ) )
proof end;

theorem Th35: :: FDIFF_6:35
for b1 being open Subset of REAL
for b2, b3 being PartFunc of REAL , REAL st b1 c= dom ((log_ number_e ) * b2) & b2 = exp - (exp * b3) & ( for b4 being Real st b4 in b1 holds
( b3 . b4 = - b4 & b2 . b4 > 0 ) ) holds
( (log_ number_e ) * b2 is_differentiable_on b1 & ( for b4 being Real st b4 in b1 holds
(((log_ number_e ) * b2) `| b1) . b4 = ((exp b4) + (exp (- b4))) / ((exp b4) - (exp (- b4))) ) )
proof end;

theorem Th36: :: FDIFF_6:36
for b1 being open Subset of REAL
for b2 being PartFunc of REAL , REAL st b1 c= dom ((2 / 3) (#) ((#R (3 / 2)) * (b2 + exp ))) & ( for b3 being Real st b3 in b1 holds
b2 . b3 = 1 ) holds
( (2 / 3) (#) ((#R (3 / 2)) * (b2 + exp )) is_differentiable_on b1 & ( for b3 being Real st b3 in b1 holds
(((2 / 3) (#) ((#R (3 / 2)) * (b2 + exp ))) `| b1) . b3 = (exp . b3) * ((1 + (exp . b3)) #R (1 / 2)) ) )
proof end;

theorem Th37: :: FDIFF_6:37
for b1 being Real
for b2 being open Subset of REAL
for b3, b4 being PartFunc of REAL , REAL st b2 c= dom ((2 / (3 * (log number_e ,b1))) (#) ((#R (3 / 2)) * (b3 + (exp * b4)))) & ( for b5 being Real st b5 in b2 holds
( b3 . b5 = 1 & b4 . b5 = b5 * (log number_e ,b1) ) ) & b1 > 0 & b1 <> 1 holds
( (2 / (3 * (log number_e ,b1))) (#) ((#R (3 / 2)) * (b3 + (exp * b4))) is_differentiable_on b2 & ( for b5 being Real st b5 in b2 holds
(((2 / (3 * (log number_e ,b1))) (#) ((#R (3 / 2)) * (b3 + (exp * b4)))) `| b2) . b5 = (b1 #R b5) * ((1 + (b1 #R b5)) #R (1 / 2)) ) )
proof end;

theorem Th38: :: FDIFF_6:38
for b1 being open Subset of REAL
for b2 being PartFunc of REAL , REAL st b1 c= dom ((- (1 / 2)) (#) (cos * b2)) & ( for b3 being Real st b3 in b1 holds
b2 . b3 = 2 * b3 ) holds
( (- (1 / 2)) (#) (cos * b2) is_differentiable_on b1 & ( for b3 being Real st b3 in b1 holds
(((- (1 / 2)) (#) (cos * b2)) `| b1) . b3 = sin (2 * b3) ) )
proof end;

theorem Th39: :: FDIFF_6:39
for b1 being open Subset of REAL
for b2 being PartFunc of REAL , REAL st b1 c= dom (2 (#) ((#R (1 / 2)) * (b2 - cos ))) & ( for b3 being Real st b3 in b1 holds
( b2 . b3 = 1 & sin . b3 > 0 & cos . b3 < 1 & cos . b3 > - 1 ) ) holds
( 2 (#) ((#R (1 / 2)) * (b2 - cos )) is_differentiable_on b1 & ( for b3 being Real st b3 in b1 holds
((2 (#) ((#R (1 / 2)) * (b2 - cos ))) `| b1) . b3 = (1 + (cos . b3)) #R (1 / 2) ) )
proof end;

theorem Th40: :: FDIFF_6:40
for b1 being open Subset of REAL
for b2 being PartFunc of REAL , REAL st b1 c= dom ((- 2) (#) ((#R (1 / 2)) * (b2 + cos ))) & ( for b3 being Real st b3 in b1 holds
( b2 . b3 = 1 & sin . b3 > 0 & cos . b3 < 1 & cos . b3 > - 1 ) ) holds
( (- 2) (#) ((#R (1 / 2)) * (b2 + cos )) is_differentiable_on b1 & ( for b3 being Real st b3 in b1 holds
(((- 2) (#) ((#R (1 / 2)) * (b2 + cos ))) `| b1) . b3 = (1 - (cos . b3)) #R (1 / 2) ) )
proof end;

Lemma20: for b1 being open Subset of REAL
for b2 being PartFunc of REAL , REAL st b1 c= dom (b2 + (2 (#) sin )) & ( for b3 being Real st b3 in b1 holds
b2 . b3 = 1 ) holds
( b2 + (2 (#) sin ) is_differentiable_on b1 & ( for b3 being Real st b3 in b1 holds
((b2 + (2 (#) sin )) `| b1) . b3 = 2 * (cos . b3) ) )
proof end;

theorem Th41: :: FDIFF_6:41
for b1 being open Subset of REAL
for b2, b3 being PartFunc of REAL , REAL st b1 c= dom ((1 / 2) (#) ((log_ number_e ) * b2)) & b2 = b3 + (2 (#) sin ) & ( for b4 being Real st b4 in b1 holds
( b3 . b4 = 1 & b2 . b4 > 0 ) ) holds
( (1 / 2) (#) ((log_ number_e ) * b2) is_differentiable_on b1 & ( for b4 being Real st b4 in b1 holds
(((1 / 2) (#) ((log_ number_e ) * b2)) `| b1) . b4 = (cos . b4) / (1 + (2 * (sin . b4))) ) )
proof end;

Lemma21: for b1 being open Subset of REAL
for b2 being PartFunc of REAL , REAL st b1 c= dom (b2 + (2 (#) cos )) & ( for b3 being Real st b3 in b1 holds
b2 . b3 = 1 ) holds
( b2 + (2 (#) cos ) is_differentiable_on b1 & ( for b3 being Real st b3 in b1 holds
((b2 + (2 (#) cos )) `| b1) . b3 = - (2 * (sin . b3)) ) )
proof end;

theorem Th42: :: FDIFF_6:42
for b1 being open Subset of REAL
for b2, b3 being PartFunc of REAL , REAL st b1 c= dom ((- (1 / 2)) (#) ((log_ number_e ) * b2)) & b2 = b3 + (2 (#) cos ) & ( for b4 being Real st b4 in b1 holds
( b3 . b4 = 1 & b2 . b4 > 0 ) ) holds
( (- (1 / 2)) (#) ((log_ number_e ) * b2) is_differentiable_on b1 & ( for b4 being Real st b4 in b1 holds
(((- (1 / 2)) (#) ((log_ number_e ) * b2)) `| b1) . b4 = (sin . b4) / (1 + (2 * (cos . b4))) ) )
proof end;

theorem Th43: :: FDIFF_6:43
for b1 being Real
for b2 being open Subset of REAL
for b3 being PartFunc of REAL , REAL st b2 c= dom ((1 / (4 * b1)) (#) (sin * b3)) & ( for b4 being Real st b4 in b2 holds
b3 . b4 = (2 * b1) * b4 ) & b1 <> 0 holds
( (1 / (4 * b1)) (#) (sin * b3) is_differentiable_on b2 & ( for b4 being Real st b4 in b2 holds
(((1 / (4 * b1)) (#) (sin * b3)) `| b2) . b4 = (1 / 2) * (cos ((2 * b1) * b4)) ) )
proof end;

theorem Th44: :: FDIFF_6:44
for b1 being Real
for b2 being open Subset of REAL
for b3, b4 being PartFunc of REAL , REAL st b2 c= dom (b3 - ((1 / (4 * b1)) (#) (sin * b4))) & ( for b5 being Real st b5 in b2 holds
( b3 . b5 = b5 / 2 & b4 . b5 = (2 * b1) * b5 ) ) & b1 <> 0 holds
( b3 - ((1 / (4 * b1)) (#) (sin * b4)) is_differentiable_on b2 & ( for b5 being Real st b5 in b2 holds
((b3 - ((1 / (4 * b1)) (#) (sin * b4))) `| b2) . b5 = (sin (b1 * b5)) ^2 ) )
proof end;

theorem Th45: :: FDIFF_6:45
for b1 being Real
for b2 being open Subset of REAL
for b3, b4 being PartFunc of REAL , REAL st b2 c= dom (b3 + ((1 / (4 * b1)) (#) (sin * b4))) & ( for b5 being Real st b5 in b2 holds
( b3 . b5 = b5 / 2 & b4 . b5 = (2 * b1) * b5 ) ) & b1 <> 0 holds
( b3 + ((1 / (4 * b1)) (#) (sin * b4)) is_differentiable_on b2 & ( for b5 being Real st b5 in b2 holds
((b3 + ((1 / (4 * b1)) (#) (sin * b4))) `| b2) . b5 = (cos (b1 * b5)) ^2 ) )
proof end;

theorem Th46: :: FDIFF_6:46
for b1 being Nat
for b2 being open Subset of REAL st b2 c= dom ((1 / b1) (#) ((#Z b1) * cos )) & b1 > 0 holds
( (1 / b1) (#) ((#Z b1) * cos ) is_differentiable_on b2 & ( for b3 being Real st b3 in b2 holds
(((1 / b1) (#) ((#Z b1) * cos )) `| b2) . b3 = - (((cos . b3) #Z (b1 - 1)) * (sin . b3)) ) )
proof end;

theorem Th47: :: FDIFF_6:47
for b1 being Nat
for b2 being open Subset of REAL st b2 c= dom (((1 / 3) (#) ((#Z 3) * cos )) - cos ) & b1 > 0 holds
( ((1 / 3) (#) ((#Z 3) * cos )) - cos is_differentiable_on b2 & ( for b3 being Real st b3 in b2 holds
((((1 / 3) (#) ((#Z 3) * cos )) - cos ) `| b2) . b3 = (sin . b3) |^ 3 ) )
proof end;

theorem Th48: :: FDIFF_6:48
for b1 being Nat
for b2 being open Subset of REAL st b2 c= dom (sin - ((1 / 3) (#) ((#Z 3) * sin ))) & b1 > 0 holds
( sin - ((1 / 3) (#) ((#Z 3) * sin )) is_differentiable_on b2 & ( for b3 being Real st b3 in b2 holds
((sin - ((1 / 3) (#) ((#Z 3) * sin ))) `| b2) . b3 = (cos . b3) |^ 3 ) )
proof end;

theorem Th49: :: FDIFF_6:49
for b1 being open Subset of REAL st b1 c= dom (sin * (log_ number_e )) holds
( sin * (log_ number_e ) is_differentiable_on b1 & ( for b2 being Real st b2 in b1 holds
((sin * (log_ number_e )) `| b1) . b2 = (cos . (log number_e ,b2)) / b2 ) )
proof end;

theorem Th50: :: FDIFF_6:50
for b1 being open Subset of REAL st b1 c= dom (- (cos * (log_ number_e ))) holds
( - (cos * (log_ number_e )) is_differentiable_on b1 & ( for b2 being Real st b2 in b1 holds
((- (cos * (log_ number_e ))) `| b1) . b2 = (sin . (log number_e ,b2)) / b2 ) )
proof end;