:: FDIFF_4 semantic presentation

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

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

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

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

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

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

theorem Th7: :: FDIFF_4:7
for b1 being Real
for b2 being open Subset of REAL
for b3, b4 being PartFunc of REAL , REAL st b2 c= dom ((id b2) + ((2 * b1) (#) b3)) & b3 = (log_ number_e ) * b4 & ( for b5 being Real st b5 in b2 holds
( b4 . b5 = b5 - b1 & b4 . b5 > 0 ) ) holds
( (id b2) + ((2 * b1) (#) b3) is_differentiable_on b2 & ( for b5 being Real st b5 in b2 holds
(((id b2) + ((2 * b1) (#) b3)) `| b2) . b5 = (b5 + b1) / (b5 - b1) ) )
proof end;

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

theorem Th9: :: FDIFF_4:9
for b1, b2 being Real
for b3 being open Subset of REAL
for b4, b5 being PartFunc of REAL , REAL st b3 c= dom ((id b3) + ((b1 + b2) (#) b4)) & b4 = (log_ number_e ) * b5 & ( for b6 being Real st b6 in b3 holds
( b5 . b6 = b6 - b2 & b5 . b6 > 0 ) ) holds
( (id b3) + ((b1 + b2) (#) b4) is_differentiable_on b3 & ( for b6 being Real st b6 in b3 holds
(((id b3) + ((b1 + b2) (#) b4)) `| b3) . b6 = (b6 + b1) / (b6 - b2) ) )
proof end;

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

theorem Th11: :: FDIFF_4:11
for b1, b2 being Real
for b3 being open Subset of REAL
for b4, b5 being PartFunc of REAL , REAL st b3 c= dom ((id b3) + ((b1 - b2) (#) b4)) & b4 = (log_ number_e ) * b5 & ( for b6 being Real st b6 in b3 holds
( b5 . b6 = b6 - b1 & b5 . b6 > 0 ) ) holds
( (id b3) + ((b1 - b2) (#) b4) is_differentiable_on b3 & ( for b6 being Real st b6 in b3 holds
(((id b3) + ((b1 - b2) (#) b4)) `| b3) . b6 = (b6 - b2) / (b6 - b1) ) )
proof end;

theorem Th12: :: FDIFF_4:12
for b1, b2, b3 being Real
for b4 being open Subset of REAL
for b5, b6 being PartFunc of REAL , REAL st b4 c= dom (b5 + (b1 (#) b6)) & ( for b7 being Real st b7 in b4 holds
b5 . b7 = b2 + (b3 * b7) ) & b6 = #Z 2 holds
( b5 + (b1 (#) b6) is_differentiable_on b4 & ( for b7 being Real st b7 in b4 holds
((b5 + (b1 (#) b6)) `| b4) . b7 = b3 + ((2 * b1) * b7) ) )
proof end;

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

theorem Th14: :: FDIFF_4:14
for b1 being Real
for b2 being open Subset of REAL
for b3 being PartFunc of REAL , REAL st b2 c= dom b3 & ( for b4 being Real st b4 in b2 holds
( b3 . b4 = b1 + b4 & b3 . b4 <> 0 ) ) holds
( b3 ^ is_differentiable_on b2 & ( for b4 being Real st b4 in b2 holds
((b3 ^ ) `| b2) . b4 = - (1 / ((b1 + b4) ^2 )) ) )
proof end;

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

theorem Th16: :: FDIFF_4:16
for b1 being Real
for b2 being open Subset of REAL
for b3 being PartFunc of REAL , REAL st b2 c= dom b3 & ( for b4 being Real st b4 in b2 holds
( b3 . b4 = b1 - b4 & b3 . b4 <> 0 ) ) holds
( b3 ^ is_differentiable_on b2 & ( for b4 being Real st b4 in b2 holds
((b3 ^ ) `| b2) . b4 = 1 / ((b1 - b4) ^2 ) ) )
proof end;

theorem Th17: :: FDIFF_4:17
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 Th18: :: FDIFF_4:18
for b1 being Real
for b2 being open Subset of REAL
for b3, b4 being PartFunc of REAL , REAL st b2 c= dom ((log_ number_e ) * (b3 + b4)) & b4 = #Z 2 & ( for b5 being Real st b5 in b2 holds
( b3 . b5 = b1 ^2 & (b3 + b4) . b5 > 0 ) ) holds
( (log_ number_e ) * (b3 + b4) is_differentiable_on b2 & ( for b5 being Real st b5 in b2 holds
(((log_ number_e ) * (b3 + b4)) `| b2) . b5 = (2 * b5) / ((b1 ^2 ) + (b5 |^ 2)) ) )
proof end;

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

theorem Th20: :: FDIFF_4:20
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 ) & b4 = #Z 3 holds
( b3 + b4 is_differentiable_on b2 & ( for b5 being Real st b5 in b2 holds
((b3 + b4) `| b2) . b5 = 3 * (b5 |^ 2) ) )
proof end;

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

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

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

theorem Th24: :: FDIFF_4:24
for b1, b2 being Real
for b3 being open Subset of REAL
for b4, b5 being PartFunc of REAL , REAL st b3 c= dom ((log_ number_e ) * (b4 / b5)) & ( for b6 being Real st b6 in b3 holds
( b4 . b6 = b6 - b1 & b4 . b6 > 0 & b5 . b6 = b6 - b2 & b5 . b6 > 0 ) ) holds
( (log_ number_e ) * (b4 / b5) is_differentiable_on b3 & ( for b6 being Real st b6 in b3 holds
(((log_ number_e ) * (b4 / b5)) `| b3) . b6 = (b1 - b2) / ((b6 - b1) * (b6 - b2)) ) )
proof end;

theorem Th25: :: FDIFF_4:25
for b1, b2 being Real
for b3 being open Subset of REAL
for b4, b5, b6 being PartFunc of REAL , REAL st b3 c= dom ((1 / (b1 - b2)) (#) b4) & b4 = (log_ number_e ) * (b5 / b6) & ( for b7 being Real st b7 in b3 holds
( b5 . b7 = b7 - b1 & b5 . b7 > 0 & b6 . b7 = b7 - b2 & b6 . b7 > 0 & b1 - b2 <> 0 ) ) holds
( (1 / (b1 - b2)) (#) b4 is_differentiable_on b3 & ( for b7 being Real st b7 in b3 holds
(((1 / (b1 - b2)) (#) b4) `| b3) . b7 = 1 / ((b7 - b1) * (b7 - b2)) ) )
proof end;

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

theorem Th27: :: FDIFF_4:27
for b1 being Real
for b2 being open Subset of REAL
for b3 being PartFunc of REAL , REAL st b2 c= dom ((#R (3 / 2)) * b3) & ( for b4 being Real st b4 in b2 holds
( b3 . b4 = b1 + b4 & b3 . b4 > 0 ) ) holds
( (#R (3 / 2)) * b3 is_differentiable_on b2 & ( for b4 being Real st b4 in b2 holds
(((#R (3 / 2)) * b3) `| b2) . b4 = (3 / 2) * ((b1 + b4) #R (1 / 2)) ) )
proof end;

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

theorem Th29: :: FDIFF_4:29
for b1 being Real
for b2 being open Subset of REAL
for b3 being PartFunc of REAL , REAL st b2 c= dom ((- (2 / 3)) (#) ((#R (3 / 2)) * b3)) & ( for b4 being Real st b4 in b2 holds
( b3 . b4 = b1 - b4 & b3 . b4 > 0 ) ) holds
( (- (2 / 3)) (#) ((#R (3 / 2)) * b3) is_differentiable_on b2 & ( for b4 being Real st b4 in b2 holds
(((- (2 / 3)) (#) ((#R (3 / 2)) * b3)) `| b2) . b4 = (b1 - b4) #R (1 / 2) ) )
proof end;

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

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

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

theorem Th33: :: FDIFF_4:33
for b1, b2 being Real
for b3 being open Subset of REAL
for b4 being PartFunc of REAL , REAL st b3 c= dom ((- (2 / (3 * b1))) (#) ((#R (3 / 2)) * b4)) & ( for b5 being Real st b5 in b3 holds
( b4 . b5 = b2 - (b1 * b5) & b1 <> 0 & b4 . b5 > 0 ) ) holds
( (- (2 / (3 * b1))) (#) ((#R (3 / 2)) * b4) is_differentiable_on b3 & ( for b5 being Real st b5 in b3 holds
(((- (2 / (3 * b1))) (#) ((#R (3 / 2)) * b4)) `| b3) . b5 = (b2 - (b1 * b5)) #R (1 / 2) ) )
proof end;

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

theorem Th35: :: FDIFF_4:35
for b1 being Real
for b2 being open Subset of REAL
for b3, b4, b5 being PartFunc of REAL , REAL st b2 c= dom (- ((#R (1 / 2)) * b3)) & b3 = b4 - b5 & b5 = #Z 2 & ( for b6 being Real st b6 in b2 holds
( b4 . b6 = b1 ^2 & b3 . b6 > 0 ) ) holds
( - ((#R (1 / 2)) * b3) is_differentiable_on b2 & ( for b6 being Real st b6 in b2 holds
((- ((#R (1 / 2)) * b3)) `| b2) . b6 = b6 * (((b1 ^2 ) - (b6 |^ 2)) #R (- (1 / 2))) ) )
proof end;

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

theorem Th37: :: FDIFF_4:37
for b1, b2 being Real
for b3 being open Subset of REAL
for b4 being PartFunc of REAL , REAL st b3 c= dom (sin * b4) & ( for b5 being Real st b5 in b3 holds
b4 . b5 = (b1 * b5) + b2 ) holds
( sin * b4 is_differentiable_on b3 & ( for b5 being Real st b5 in b3 holds
((sin * b4) `| b3) . b5 = b1 * (cos . ((b1 * b5) + b2)) ) )
proof end;

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

theorem Th39: :: FDIFF_4:39
for b1 being open Subset of REAL st ( for b2 being Real st b2 in b1 holds
cos . b2 <> 0 ) holds
( cos ^ is_differentiable_on b1 & ( for b2 being Real st b2 in b1 holds
((cos ^ ) `| b1) . b2 = (sin . b2) / ((cos . b2) ^2 ) ) )
proof end;

theorem Th40: :: FDIFF_4:40
for b1 being open Subset of REAL st ( for b2 being Real st b2 in b1 holds
sin . b2 <> 0 ) holds
( sin ^ is_differentiable_on b1 & ( for b2 being Real st b2 in b1 holds
((sin ^ ) `| b1) . b2 = - ((cos . b2) / ((sin . b2) ^2 )) ) )
proof end;

theorem Th41: :: FDIFF_4:41
for b1 being open Subset of REAL st b1 c= dom (sin (#) cos ) holds
( sin (#) cos is_differentiable_on b1 & ( for b2 being Real st b2 in b1 holds
((sin (#) cos ) `| b1) . b2 = cos (2 * b2) ) )
proof end;

theorem Th42: :: FDIFF_4:42
for b1 being open Subset of REAL st b1 c= dom ((log_ number_e ) * cos ) & ( for b2 being Real st b2 in b1 holds
cos . b2 > 0 ) holds
( (log_ number_e ) * cos is_differentiable_on b1 & ( for b2 being Real st b2 in b1 holds
(((log_ number_e ) * cos ) `| b1) . b2 = - (tan b2) ) )
proof end;

theorem Th43: :: FDIFF_4:43
for b1 being open Subset of REAL st b1 c= dom ((log_ number_e ) * sin ) & ( for b2 being Real st b2 in b1 holds
sin . b2 > 0 ) holds
( (log_ number_e ) * sin is_differentiable_on b1 & ( for b2 being Real st b2 in b1 holds
(((log_ number_e ) * sin ) `| b1) . b2 = cot b2 ) )
proof end;

theorem Th44: :: FDIFF_4:44
for b1 being open Subset of REAL st b1 c= dom ((- (id b1)) (#) cos ) holds
( (- (id b1)) (#) cos is_differentiable_on b1 & ( for b2 being Real st b2 in b1 holds
(((- (id b1)) (#) cos ) `| b1) . b2 = (- (cos . b2)) + (b2 * (sin . b2)) ) )
proof end;

theorem Th45: :: FDIFF_4:45
for b1 being open Subset of REAL st b1 c= dom ((id b1) (#) sin ) holds
( (id b1) (#) sin is_differentiable_on b1 & ( for b2 being Real st b2 in b1 holds
(((id b1) (#) sin ) `| b1) . b2 = (sin . b2) + (b2 * (cos . b2)) ) )
proof end;

theorem Th46: :: FDIFF_4:46
for b1 being open Subset of REAL st b1 c= dom (((- (id b1)) (#) cos ) + sin ) holds
( ((- (id b1)) (#) cos ) + sin is_differentiable_on b1 & ( for b2 being Real st b2 in b1 holds
((((- (id b1)) (#) cos ) + sin ) `| b1) . b2 = b2 * (sin . b2) ) )
proof end;

theorem Th47: :: FDIFF_4:47
for b1 being open Subset of REAL st b1 c= dom (((id b1) (#) sin ) + cos ) holds
( ((id b1) (#) sin ) + cos is_differentiable_on b1 & ( for b2 being Real st b2 in b1 holds
((((id b1) (#) sin ) + cos ) `| b1) . b2 = b2 * (cos . b2) ) )
proof end;

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

theorem Th49: :: FDIFF_4:49
for b1 being open Subset of REAL st b1 c= dom ((1 / 2) (#) ((#Z 2) * sin )) holds
( (1 / 2) (#) ((#Z 2) * sin ) is_differentiable_on b1 & ( for b2 being Real st b2 in b1 holds
(((1 / 2) (#) ((#Z 2) * sin )) `| b1) . b2 = (sin . b2) * (cos . b2) ) )
proof end;

theorem Th50: :: FDIFF_4:50
for b1 being open Subset of REAL st b1 c= dom (sin + ((1 / 2) (#) ((#Z 2) * sin ))) & ( for b2 being Real st b2 in b1 holds
( sin . b2 > 0 & sin . b2 < 1 ) ) holds
( sin + ((1 / 2) (#) ((#Z 2) * sin )) is_differentiable_on b1 & ( for b2 being Real st b2 in b1 holds
((sin + ((1 / 2) (#) ((#Z 2) * sin ))) `| b1) . b2 = ((cos . b2) |^ 3) / (1 - (sin . b2)) ) )
proof end;

theorem Th51: :: FDIFF_4:51
for b1 being open Subset of REAL st b1 c= dom (((1 / 2) (#) ((#Z 2) * sin )) - cos ) & ( for b2 being Real st b2 in b1 holds
( sin . b2 > 0 & cos . b2 < 1 ) ) holds
( ((1 / 2) (#) ((#Z 2) * sin )) - cos is_differentiable_on b1 & ( for b2 being Real st b2 in b1 holds
((((1 / 2) (#) ((#Z 2) * sin )) - cos ) `| b1) . b2 = ((sin . b2) |^ 3) / (1 - (cos . b2)) ) )
proof end;

theorem Th52: :: FDIFF_4:52
for b1 being open Subset of REAL st b1 c= dom (sin - ((1 / 2) (#) ((#Z 2) * sin ))) & ( for b2 being Real st b2 in b1 holds
( sin . b2 > 0 & sin . b2 > - 1 ) ) holds
( sin - ((1 / 2) (#) ((#Z 2) * sin )) is_differentiable_on b1 & ( for b2 being Real st b2 in b1 holds
((sin - ((1 / 2) (#) ((#Z 2) * sin ))) `| b1) . b2 = ((cos . b2) |^ 3) / (1 + (sin . b2)) ) )
proof end;

theorem Th53: :: FDIFF_4:53
for b1 being open Subset of REAL st b1 c= dom ((- cos ) - ((1 / 2) (#) ((#Z 2) * sin ))) & ( for b2 being Real st b2 in b1 holds
( sin . b2 > 0 & cos . b2 > - 1 ) ) holds
( (- cos ) - ((1 / 2) (#) ((#Z 2) * sin )) is_differentiable_on b1 & ( for b2 being Real st b2 in b1 holds
(((- cos ) - ((1 / 2) (#) ((#Z 2) * sin ))) `| b1) . b2 = ((sin . b2) |^ 3) / (1 + (cos . b2)) ) )
proof end;

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

theorem Th55: :: FDIFF_4:55
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 - 1 ) holds
( exp (#) b2 is_differentiable_on b1 & ( for b3 being Real st b3 in b1 holds
((exp (#) b2) `| b1) . b3 = b3 * (exp . b3) ) )
proof end;

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

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