begin
definition
let S,
T be non
trivial RealNormSpace;
let f be
PartFunc of
S,
T;
let X be
set ;
assume A1:
f is_differentiable_on X
;
existence
ex b1 being PartFunc of S,(R_NormSpace_of_BoundedLinearOperators (S,T)) st
( dom b1 = X & ( for x being Point of S st x in X holds
b1 /. x = diff (f,x) ) )
uniqueness
for b1, b2 being PartFunc of S,(R_NormSpace_of_BoundedLinearOperators (S,T)) st dom b1 = X & ( for x being Point of S st x in X holds
b1 /. x = diff (f,x) ) & dom b2 = X & ( for x being Point of S st x in X holds
b2 /. x = diff (f,x) ) holds
b1 = b2
end;
:: RCOMP_1:37 --> NFCONT_1:4