:: NDIFF_1 semantic presentation

theorem Th1: :: NDIFF_1:1
for b1 being RealNormSpace
for b2 being Point of b1
for b3, b4 being Neighbourhood of b2 ex b5 being Neighbourhood of b2 st
( b5 c= b3 & b5 c= b4 )
proof end;

theorem Th2: :: NDIFF_1:2
for b1 being RealNormSpace
for b2 being Subset of b1 st b2 is open holds
for b3 being Point of b1 st b3 in b2 holds
ex b4 being Neighbourhood of b3 st b4 c= b2
proof end;

theorem Th3: :: NDIFF_1:3
for b1 being RealNormSpace
for b2 being Subset of b1 st b2 is open holds
for b3 being Point of b1 st b3 in b2 holds
ex b4 being Real st
( 0 < b4 & { b5 where B is Point of b1 : ||.(b5 - b3).|| < b4 } c= b2 )
proof end;

theorem Th4: :: NDIFF_1:4
for b1 being RealNormSpace
for b2 being Subset of b1 st ( for b3 being Point of b1 st b3 in b2 holds
ex b4 being Neighbourhood of b3 st b4 c= b2 ) holds
b2 is open
proof end;

theorem Th5: :: NDIFF_1:5
for b1 being RealNormSpace
for b2 being Subset of b1 holds
( ( for b3 being Point of b1 st b3 in b2 holds
ex b4 being Neighbourhood of b3 st b4 c= b2 ) iff b2 is open ) by Th2, Th4;

definition
let c1 be ZeroStr ;
let c2 be sequence of c1;
attr a2 is being_not_0 means :Def1: :: NDIFF_1:def 1
 rng a2 c= the carrier of a1 \ {(0. a1)};
end;

:: deftheorem Def1 defines being_not_0 NDIFF_1:def 1 :
for b1 being ZeroStr
for b2 being sequence of b1 holds
( b2 is being_not_0 iff rng b2 c= the carrier of b1 \ {(0. b1)} );

notation
let c1 be ZeroStr ;
let c2 be sequence of c1;
synonym c2 is_not_0 for being_not_0 c2;
end;

theorem Th6: :: NDIFF_1:6
for b1 being RealNormSpace
for b2 being sequence of b1 holds
( b2 is being_not_0 iff for b3 being set st b3 in NAT holds
b2 . b3 <> 0. b1 )
proof end;

theorem Th7: :: NDIFF_1:7
for b1 being RealNormSpace
for b2 being sequence of b1 holds
( b2 is being_not_0 iff for b3 being Nat holds b2 . b3 <> 0. b1 )
proof end;

definition
let c1 be RealLinearSpace;
let c2 be sequence of c1;
let c3 be Real_Sequence;
func c3 (#) c2 -> sequence of a1 means :Def2: :: NDIFF_1:def 2
for b1 being Nat holds a4 . b1 = (a3 . b1) * (a2 . b1);
existence
ex b1 being sequence of c1 st
for b2 being Nat holds b1 . b2 = (c3 . b2) * (c2 . b2)
proof end;
uniqueness
for b1, b2 being sequence of c1 st ( for b3 being Nat holds b1 . b3 = (c3 . b3) * (c2 . b3) ) & ( for b3 being Nat holds b2 . b3 = (c3 . b3) * (c2 . b3) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def2 defines (#) NDIFF_1:def 2 :
for b1 being RealLinearSpace
for b2 being sequence of b1
for b3 being Real_Sequence
for b4 being sequence of b1 holds
( b4 = b3 (#) b2 iff for b5 being Nat holds b4 . b5 = (b3 . b5) * (b2 . b5) );

definition
let c1 be RealLinearSpace;
let c2 be Point of c1;
let c3 be Real_Sequence;
func c3 * c2 -> sequence of a1 means :Def3: :: NDIFF_1:def 3
for b1 being Nat holds a4 . b1 = (a3 . b1) * a2;
existence
ex b1 being sequence of c1 st
for b2 being Nat holds b1 . b2 = (c3 . b2) * c2
proof end;
uniqueness
for b1, b2 being sequence of c1 st ( for b3 being Nat holds b1 . b3 = (c3 . b3) * c2 ) & ( for b3 being Nat holds b2 . b3 = (c3 . b3) * c2 ) holds
b1 = b2
proof end;
end;

:: deftheorem Def3 defines * NDIFF_1:def 3 :
for b1 being RealLinearSpace
for b2 being Point of b1
for b3 being Real_Sequence
for b4 being sequence of b1 holds
( b4 = b3 * b2 iff for b5 being Nat holds b4 . b5 = (b3 . b5) * b2 );

theorem Th8: :: NDIFF_1:8
for b1 being RealNormSpace
for b2 being sequence of b1
for b3, b4 being Real_Sequence holds (b3 + b4) (#) b2 = (b3 (#) b2) + (b4 (#) b2)
proof end;

theorem Th9: :: NDIFF_1:9
for b1 being RealNormSpace
for b2 being Real_Sequence
for b3, b4 being sequence of b1 holds b2 (#) (b3 + b4) = (b2 (#) b3) + (b2 (#) b4)
proof end;

theorem Th10: :: NDIFF_1:10
for b1 being Real
for b2 being RealNormSpace
for b3 being sequence of b2
for b4 being Real_Sequence holds b1 * (b4 (#) b3) = b4 (#) (b1 * b3)
proof end;

theorem Th11: :: NDIFF_1:11
for b1 being RealNormSpace
for b2 being sequence of b1
for b3, b4 being Real_Sequence holds (b3 - b4) (#) b2 = (b3 (#) b2) - (b4 (#) b2)
proof end;

theorem Th12: :: NDIFF_1:12
for b1 being RealNormSpace
for b2 being Real_Sequence
for b3, b4 being sequence of b1 holds b2 (#) (b3 - b4) = (b2 (#) b3) - (b2 (#) b4)
proof end;

theorem Th13: :: NDIFF_1:13
for b1 being RealNormSpace
for b2 being Real_Sequence
for b3 being sequence of b1 st b2 is convergent & b3 is convergent holds
b2 (#) b3 is convergent
proof end;

theorem Th14: :: NDIFF_1:14
for b1 being RealNormSpace
for b2 being Real_Sequence
for b3 being sequence of b1 st b2 is convergent & b3 is convergent holds
lim (b2 (#) b3) = (lim b2) * (lim b3)
proof end;

theorem Th15: :: NDIFF_1:15
for b1 being Nat
for b2 being RealNormSpace
for b3, b4 being sequence of b2 holds (b3 + b4) ^\ b1 = (b3 ^\ b1) + (b4 ^\ b1)
proof end;

theorem Th16: :: NDIFF_1:16
for b1 being Nat
for b2 being RealNormSpace
for b3, b4 being sequence of b2 holds (b3 - b4) ^\ b1 = (b3 ^\ b1) - (b4 ^\ b1)
proof end;

theorem Th17: :: NDIFF_1:17
for b1 being Nat
for b2 being RealNormSpace
for b3 being sequence of b2 st b3 is_not_0 holds
b3 ^\ b1 is_not_0
proof end;

theorem Th18: :: NDIFF_1:18
for b1 being Nat
for b2 being RealNormSpace
for b3 being sequence of b2 holds b3 ^\ b1 is subsequence of b3
proof end;

theorem Th19: :: NDIFF_1:19
for b1 being RealNormSpace
for b2, b3 being sequence of b1 st b2 is constant & b3 is subsequence of b2 holds
b3 is constant
proof end;

theorem Th20: :: NDIFF_1:20
for b1 being RealNormSpace
for b2, b3 being sequence of b1 st b2 is constant & b3 is subsequence of b2 holds
b2 = b3
proof end;

definition
let c1 be RealNormSpace;
let c2 be sequence of c1;
attr a2 is convergent_to_0 means :Def4: :: NDIFF_1:def 4
( a2 is_not_0 & a2 is convergent & lim a2 = 0. a1 );
end;

:: deftheorem Def4 defines convergent_to_0 NDIFF_1:def 4 :
for b1 being RealNormSpace
for b2 being sequence of b1 holds
( b2 is convergent_to_0 iff ( b2 is_not_0 & b2 is convergent & lim b2 = 0. b1 ) );

theorem Th21: :: NDIFF_1:21
for b1 being RealNormSpace
for b2 being sequence of b1 st b2 is constant holds
( b2 is convergent & ( for b3 being Nat holds lim b2 = b2 . b3 ) )
proof end;

theorem Th22: :: NDIFF_1:22
for b1 being RealNormSpace
for b2 being sequence of b1
for b3 being Point of b1
for b4 being Real st 0 < b4 & ( for b5 being Nat holds b2 . b5 = (1 / (b5 + b4)) * b3 ) holds
b2 is convergent
proof end;

theorem Th23: :: NDIFF_1:23
for b1 being RealNormSpace
for b2 being sequence of b1
for b3 being Point of b1
for b4 being Real st 0 < b4 & ( for b5 being Nat holds b2 . b5 = (1 / (b5 + b4)) * b3 ) holds
lim b2 = 0. b1
proof end;

theorem Th24: :: NDIFF_1:24
for b1 being RealNormSpace
for b2 being convergent_to_0 Real_Sequence
for b3 being Point of b1 st b3 <> 0. b1 holds
b2 * b3 is convergent_to_0
proof end;

theorem Th25: :: NDIFF_1:25
for b1 being RealNormSpace
for b2 being Subset of b1 holds
( ( for b3 being Point of b1 holds
( b3 in b2 iff b3 in the carrier of b1 ) ) iff b2 = the carrier of b1 )
proof end;

registration
let c1 be non trivial RealNormSpace;
cluster convergent_to_0 Relation of NAT ,the carrier of a1;
existence
ex b1 being sequence of c1 st b1 is convergent_to_0
proof end;
end;

registration
let c1 be non trivial RealNormSpace;
cluster V49 Relation of NAT ,the carrier of a1;
existence
ex b1 being sequence of c1 st b1 is constant
proof end;
end;

definition
let c1, c2 be non trivial RealNormSpace;
let c3 be PartFunc of c1,c2;
attr a3 is REST-like means :Def5: :: NDIFF_1:def 5
( a3 is total & ( for b1 being convergent_to_0 sequence of a1 holds
( (||.b1.|| " ) (#) (a3 * b1) is convergent & lim ((||.b1.|| " ) (#) (a3 * b1)) = 0. a2 ) ) );
end;

:: deftheorem Def5 defines REST-like NDIFF_1:def 5 :
for b1, b2 being non trivial RealNormSpace
for b3 being PartFunc of b1,b2 holds
( b3 is REST-like iff ( b3 is total & ( for b4 being convergent_to_0 sequence of b1 holds
( (||.b4.|| " ) (#) (b3 * b4) is convergent & lim ((||.b4.|| " ) (#) (b3 * b4)) = 0. b2 ) ) ) );

registration
let c1, c2 be non trivial RealNormSpace;
cluster REST-like Relation of the carrier of a1,the carrier of a2;
existence
ex b1 being PartFunc of c1,c2 st b1 is REST-like
proof end;
end;

definition
let c1, c2 be non trivial RealNormSpace;
mode REST of a1,a2 is REST-like PartFunc of a1,a2;
end;

theorem Th26: :: NDIFF_1:26
for b1, b2 being non trivial RealNormSpace
for b3 being PartFunc of b1,b2 st b3 is total holds
( b3 is REST-like iff for b4 being Real st b4 > 0 holds
ex b5 being Real st
( b5 > 0 & ( for b6 being Point of b1 st b6 <> 0. b1 & ||.b6.|| < b5 holds
(||.b6.|| " ) * ||.(b3 /. b6).|| < b4 ) ) )
proof end;

theorem Th27: :: NDIFF_1:27
for b1, b2 being non trivial RealNormSpace
for b3 being REST of b1,b2
for b4 being convergent_to_0 sequence of b1 holds
( b3 * b4 is convergent & lim (b3 * b4) = 0. b2 )
proof end;

theorem Th28: :: NDIFF_1:28
for b1 being Nat
for b2 being non trivial RealNormSpace
for b3 being sequence of b2 holds rng (b3 ^\ b1) c= rng b3
proof end;

theorem Th29: :: NDIFF_1:29
for b1 being Nat
for b2, b3 being non trivial RealNormSpace
for b4 being PartFunc of b2,b3
for b5 being sequence of b2 st rng b5 c= dom b4 holds
(b4 * b5) ^\ b1 = b4 * (b5 ^\ b1)
proof end;

theorem Th30: :: NDIFF_1:30
for b1, b2 being non trivial RealNormSpace
for b3, b4 being PartFunc of b1,b2
for b5 being sequence of b1 st b3 is total & b4 is total holds
( (b3 + b4) * b5 = (b3 * b5) + (b4 * b5) & (b3 - b4) * b5 = (b3 * b5) - (b4 * b5) )
proof end;

theorem Th31: :: NDIFF_1:31
for b1, b2 being non trivial RealNormSpace
for b3 being PartFunc of b1,b2
for b4 being sequence of b1
for b5 being Real st b3 is total holds
(b5 (#) b3) * b4 = b5 * (b3 * b4)
proof end;

theorem Th32: :: NDIFF_1:32
for b1, b2 being non trivial RealNormSpace
for b3 being PartFunc of b2,b1
for b4 being Point of b2 holds
( b3 is_continuous_in b4 iff ( b4 in dom b3 & ( for b5 being sequence of b2 st rng b5 c= dom b3 & b5 is convergent & lim b5 = b4 & ( for b6 being Nat holds b5 . b6 <> b4 ) holds
( b3 * b5 is convergent & b3 /. b4 = lim (b3 * b5) ) ) ) )
proof end;

theorem Th33: :: NDIFF_1:33
for b1, b2 being non trivial RealNormSpace
for b3, b4 being REST of b2,b1 holds
( b3 + b4 is REST of b2,b1 & b3 - b4 is REST of b2,b1 )
proof end;

theorem Th34: :: NDIFF_1:34
for b1, b2 being non trivial RealNormSpace
for b3 being Real
for b4 being REST of b2,b1 holds b3 (#) b4 is REST of b2,b1
proof end;

definition
let c1, c2 be non trivial RealNormSpace;
let c3 be PartFunc of c1,c2;
let c4 be Point of c1;
pred c3 is_differentiable_in c4 means :Def6: :: NDIFF_1:def 6
ex b1 being Neighbourhood of a4 st
( b1 c= dom a3 & ex b2 being Point of (R_NormSpace_of_BoundedLinearOperators a1,a2)ex b3 being REST of a1,a2 st
for b4 being Point of a1 st b4 in b1 holds
(a3 /. b4) - (a3 /. a4) = (b2 . (b4 - a4)) + (b3 /. (b4 - a4)) );
end;

:: deftheorem Def6 defines is_differentiable_in NDIFF_1:def 6 :
for b1, b2 being non trivial RealNormSpace
for b3 being PartFunc of b1,b2
for b4 being Point of b1 holds
( b3 is_differentiable_in b4 iff ex b5 being Neighbourhood of b4 st
( b5 c= dom b3 & ex b6 being Point of (R_NormSpace_of_BoundedLinearOperators b1,b2)ex b7 being REST of b1,b2 st
for b8 being Point of b1 st b8 in b5 holds
(b3 /. b8) - (b3 /. b4) = (b6 . (b8 - b4)) + (b7 /. (b8 - b4)) ) );

definition
let c1, c2 be non trivial RealNormSpace;
let c3 be PartFunc of c1,c2;
let c4 be Point of c1;
assume E34: c3 is_differentiable_in c4 ;
func diff c3,c4 -> Point of (R_NormSpace_of_BoundedLinearOperators a1,a2) means :Def7: :: NDIFF_1:def 7
ex b1 being Neighbourhood of a4 st
( b1 c= dom a3 & ex b2 being REST of a1,a2 st
for b3 being Point of a1 st b3 in b1 holds
(a3 /. b3) - (a3 /. a4) = (a5 . (b3 - a4)) + (b2 /. (b3 - a4)) );
existence
ex b1 being Point of (R_NormSpace_of_BoundedLinearOperators c1,c2)ex b2 being Neighbourhood of c4 st
( b2 c= dom c3 & ex b3 being REST of c1,c2 st
for b4 being Point of c1 st b4 in b2 holds
(c3 /. b4) - (c3 /. c4) = (b1 . (b4 - c4)) + (b3 /. (b4 - c4)) )
proof end;
uniqueness
for b1, b2 being Point of (R_NormSpace_of_BoundedLinearOperators c1,c2) st ex b3 being Neighbourhood of c4 st
( b3 c= dom c3 & ex b4 being REST of c1,c2 st
for b5 being Point of c1 st b5 in b3 holds
(c3 /. b5) - (c3 /. c4) = (b1 . (b5 - c4)) + (b4 /. (b5 - c4)) ) & ex b3 being Neighbourhood of c4 st
( b3 c= dom c3 & ex b4 being REST of c1,c2 st
for b5 being Point of c1 st b5 in b3 holds
(c3 /. b5) - (c3 /. c4) = (b2 . (b5 - c4)) + (b4 /. (b5 - c4)) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def7 defines diff NDIFF_1:def 7 :
for b1, b2 being non trivial RealNormSpace
for b3 being PartFunc of b1,b2
for b4 being Point of b1 st b3 is_differentiable_in b4 holds
for b5 being Point of (R_NormSpace_of_BoundedLinearOperators b1,b2) holds
( b5 = diff b3,b4 iff ex b6 being Neighbourhood of b4 st
( b6 c= dom b3 & ex b7 being REST of b1,b2 st
for b8 being Point of b1 st b8 in b6 holds
(b3 /. b8) - (b3 /. b4) = (b5 . (b8 - b4)) + (b7 /. (b8 - b4)) ) );

definition
let c1 be set ;
let c2, c3 be non trivial RealNormSpace;
let c4 be PartFunc of c2,c3;
pred c4 is_differentiable_on c1 means :Def8: :: NDIFF_1:def 8
( a1 c= dom a4 & ( for b1 being Point of a2 st b1 in a1 holds
a4 | a1 is_differentiable_in b1 ) );
end;

:: deftheorem Def8 defines is_differentiable_on NDIFF_1:def 8 :
for b1 being set
for b2, b3 being non trivial RealNormSpace
for b4 being PartFunc of b2,b3 holds
( b4 is_differentiable_on b1 iff ( b1 c= dom b4 & ( for b5 being Point of b2 st b5 in b1 holds
b4 | b1 is_differentiable_in b5 ) ) );

theorem Th35: :: NDIFF_1:35
for b1 being set
for b2, b3 being non trivial RealNormSpace
for b4 being PartFunc of b2,b3 st b4 is_differentiable_on b1 holds
b1 is Subset of b2
proof end;

theorem Th36: :: NDIFF_1:36
for b1, b2 being non trivial RealNormSpace
for b3 being PartFunc of b1,b2
for b4 being Subset of b1 st b4 is open holds
( b3 is_differentiable_on b4 iff ( b4 c= dom b3 & ( for b5 being Point of b1 st b5 in b4 holds
b3 is_differentiable_in b5 ) ) )
proof end;

theorem Th37: :: NDIFF_1:37
for b1, b2 being non trivial RealNormSpace
for b3 being PartFunc of b1,b2
for b4 being Subset of b1 st b3 is_differentiable_on b4 holds
b4 is open
proof end;

definition
let c1, c2 be non trivial RealNormSpace;
let c3 be PartFunc of c1,c2;
let c4 be set ;
assume E38: c3 is_differentiable_on c4 ;
func c3 `| c4 -> PartFunc of a1,(R_NormSpace_of_BoundedLinearOperators a1,a2) means :Def9: :: NDIFF_1:def 9
( dom a5 = a4 & ( for b1 being Point of a1 st b1 in a4 holds
a5 /. b1 = diff a3,b1 ) );
existence
ex b1 being PartFunc of c1,(R_NormSpace_of_BoundedLinearOperators c1,c2) st
( dom b1 = c4 & ( for b2 being Point of c1 st b2 in c4 holds
b1 /. b2 = diff c3,b2 ) )
proof end;
uniqueness
for b1, b2 being PartFunc of c1,(R_NormSpace_of_BoundedLinearOperators c1,c2) st dom b1 = c4 & ( for b3 being Point of c1 st b3 in c4 holds
b1 /. b3 = diff c3,b3 ) & dom b2 = c4 & ( for b3 being Point of c1 st b3 in c4 holds
b2 /. b3 = diff c3,b3 ) holds
b1 = b2
proof end;
end;

:: deftheorem Def9 defines `| NDIFF_1:def 9 :
for b1, b2 being non trivial RealNormSpace
for b3 being PartFunc of b1,b2
for b4 being set st b3 is_differentiable_on b4 holds
for b5 being PartFunc of b1,(R_NormSpace_of_BoundedLinearOperators b1,b2) holds
( b5 = b3 `| b4 iff ( dom b5 = b4 & ( for b6 being Point of b1 st b6 in b4 holds
b5 /. b6 = diff b3,b6 ) ) );

theorem Th38: :: NDIFF_1:38
for b1, b2 being non trivial RealNormSpace
for b3 being PartFunc of b1,b2
for b4 being Subset of b1 st b4 is open & b4 c= dom b3 & ex b5 being Point of b2 st rng b3 = {b5} holds
( b3 is_differentiable_on b4 & ( for b5 being Point of b1 st b5 in b4 holds
(b3 `| b4) /. b5 = 0. (R_NormSpace_of_BoundedLinearOperators b1,b2) ) )
proof end;

registration
let c1 be non trivial RealNormSpace;
let c2 be convergent_to_0 sequence of c1;
let c3 be Nat;
cluster a2 ^\ a3 -> convergent_to_0 ;
coherence
c2 ^\ c3 is convergent_to_0
proof end;
end;

registration
let c1 be non trivial RealNormSpace;
let c2 be V49 sequence of c1;
let c3 be Nat;
cluster a2 ^\ a3 -> V49 ;
coherence
c2 ^\ c3 is constant
proof end;
end;

theorem Th39: :: NDIFF_1:39
for b1, b2 being non trivial RealNormSpace
for b3 being PartFunc of b1,b2
for b4 being Point of b1
for b5 being Neighbourhood of b4 st b3 is_differentiable_in b4 & b5 c= dom b3 holds
for b6 being convergent_to_0 sequence of b1
for b7 being V49 sequence of b1 st rng b7 = {b4} & rng (b6 + b7) c= b5 holds
( (b3 * (b6 + b7)) - (b3 * b7) is convergent & lim ((b3 * (b6 + b7)) - (b3 * b7)) = 0. b2 )
proof end;

theorem Th40: :: NDIFF_1:40
for b1, b2 being non trivial RealNormSpace
for b3, b4 being PartFunc of b2,b1
for b5 being Point of b2 st b3 is_differentiable_in b5 & b4 is_differentiable_in b5 holds
( b3 + b4 is_differentiable_in b5 & diff (b3 + b4),b5 = (diff b3,b5) + (diff b4,b5) )
proof end;

theorem Th41: :: NDIFF_1:41
for b1, b2 being non trivial RealNormSpace
for b3, b4 being PartFunc of b2,b1
for b5 being Point of b2 st b3 is_differentiable_in b5 & b4 is_differentiable_in b5 holds
( b3 - b4 is_differentiable_in b5 & diff (b3 - b4),b5 = (diff b3,b5) - (diff b4,b5) )
proof end;

theorem Th42: :: NDIFF_1:42
for b1, b2 being non trivial RealNormSpace
for b3 being Real
for b4 being PartFunc of b2,b1
for b5 being Point of b2 st b4 is_differentiable_in b5 holds
( b3 (#) b4 is_differentiable_in b5 & diff (b3 (#) b4),b5 = b3 * (diff b4,b5) )
proof end;

theorem Th43: :: NDIFF_1:43
for b1 being non trivial RealNormSpace
for b2 being PartFunc of b1,b1
for b3 being Subset of b1 st b3 is open & b3 c= dom b2 & b2 | b3 = id b3 holds
( b2 is_differentiable_on b3 & ( for b4 being Point of b1 st b4 in b3 holds
(b2 `| b3) /. b4 = id the carrier of b1 ) )
proof end;

theorem Th44: :: NDIFF_1:44
for b1, b2 being non trivial RealNormSpace
for b3 being Subset of b1 st b3 is open holds
for b4, b5 being PartFunc of b1,b2 st b3 c= dom (b4 + b5) & b4 is_differentiable_on b3 & b5 is_differentiable_on b3 holds
( b4 + b5 is_differentiable_on b3 & ( for b6 being Point of b1 st b6 in b3 holds
((b4 + b5) `| b3) /. b6 = (diff b4,b6) + (diff b5,b6) ) )
proof end;

theorem Th45: :: NDIFF_1:45
for b1, b2 being non trivial RealNormSpace
for b3 being Subset of b1 st b3 is open holds
for b4, b5 being PartFunc of b1,b2 st b3 c= dom (b4 - b5) & b4 is_differentiable_on b3 & b5 is_differentiable_on b3 holds
( b4 - b5 is_differentiable_on b3 & ( for b6 being Point of b1 st b6 in b3 holds
((b4 - b5) `| b3) /. b6 = (diff b4,b6) - (diff b5,b6) ) )
proof end;

theorem Th46: :: NDIFF_1:46
for b1, b2 being non trivial RealNormSpace
for b3 being Subset of b1 st b3 is open holds
for b4 being Real
for b5 being PartFunc of b1,b2 st b3 c= dom (b4 (#) b5) & b5 is_differentiable_on b3 holds
( b4 (#) b5 is_differentiable_on b3 & ( for b6 being Point of b1 st b6 in b3 holds
((b4 (#) b5) `| b3) /. b6 = b4 * (diff b5,b6) ) )
proof end;

theorem Th47: :: NDIFF_1:47
for b1, b2 being non trivial RealNormSpace
for b3 being PartFunc of b1,b2
for b4 being Subset of b1 st b4 is open & b4 c= dom b3 & b3 is_constant_on b4 holds
( b3 is_differentiable_on b4 & ( for b5 being Point of b1 st b5 in b4 holds
(b3 `| b4) /. b5 = 0. (R_NormSpace_of_BoundedLinearOperators b1,b2) ) )
proof end;

theorem Th48: :: NDIFF_1:48
for b1 being non trivial RealNormSpace
for b2 being PartFunc of b1,b1
for b3 being Real
for b4 being Point of b1
for b5 being Subset of b1 st b5 is open & b5 c= dom b2 & ( for b6 being Point of b1 st b6 in b5 holds
b2 /. b6 = (b3 * b6) + b4 ) holds
( b2 is_differentiable_on b5 & ( for b6 being Point of b1 st b6 in b5 holds
(b2 `| b5) /. b6 = b3 * (FuncUnit b1) ) )
proof end;

theorem Th49: :: NDIFF_1:49
for b1, b2 being non trivial RealNormSpace
for b3 being PartFunc of b2,b1
for b4 being Point of b2 st b3 is_differentiable_in b4 holds
b3 is_continuous_in b4
proof end;

theorem Th50: :: NDIFF_1:50
for b1 being set
for b2, b3 being non trivial RealNormSpace
for b4 being PartFunc of b2,b3 st b4 is_differentiable_on b1 holds
b4 is_continuous_on b1
proof end;

theorem Th51: :: NDIFF_1:51
for b1 being set
for b2, b3 being non trivial RealNormSpace
for b4 being PartFunc of b3,b2
for b5 being Subset of b3 st b5 is open & b4 is_differentiable_on b1 & b5 c= b1 holds
b4 is_differentiable_on b5
proof end;

theorem Th52: :: NDIFF_1:52
for b1, b2 being non trivial RealNormSpace
for b3 being PartFunc of b2,b1
for b4 being Point of b2 st b3 is_differentiable_in b4 holds
ex b5 being Neighbourhood of b4 st
( b5 c= dom b3 & ex b6 being REST of b2,b1 st
( b6 /. (0. b2) = 0. b1 & b6 is_continuous_in 0. b2 & ( for b7 being Point of b2 st b7 in b5 holds
(b3 /. b7) - (b3 /. b4) = ((diff b3,b4) . (b7 - b4)) + (b6 /. (b7 - b4)) ) ) )
proof end;