environ
vocabularies HIDDEN, NUMBERS, SUBSET_1, REAL_1, NORMSP_1, SEQ_1, NAT_1, PRE_TOPC, RCOMP_1, TARSKI, CARD_1, ARYTM_3, ARYTM_1, XXREAL_0, RELAT_1, FUNCT_1, SEQ_2, ORDINAL2, STRUCT_0, VALUED_0, SUPINF_2, RLVECT_1, VALUED_1, COMPLEX1, XXREAL_2, FDIFF_1, ZFMISC_1, PARTFUN1, FUNCOP_1, FUNCT_2, LOPBAN_1, XBOOLE_0, FCONT_1, RSSPACE, NFCONT_1, CFCONT_1, LOPBAN_2;
notations HIDDEN, TARSKI, SUBSET_1, FUNCT_1, RELSET_1, PARTFUN1, FUNCT_2, PRE_TOPC, XCMPLX_0, XXREAL_0, XREAL_0, COMPLEX1, ORDINAL1, NUMBERS, REAL_1, NAT_1, RLVECT_1, STRUCT_0, FUNCOP_1, VALUED_0, VALUED_1, SEQ_1, SEQ_2, VFUNCT_1, NORMSP_0, NORMSP_1, RSSPACE, LOPBAN_1, LOPBAN_2, NFCONT_1, FDIFF_1, RECDEF_1;
definitions TARSKI, XBOOLE_0, NFCONT_1, NORMSP_1, STRUCT_0;
theorems TARSKI, ABSVALUE, XBOOLE_0, XBOOLE_1, SUBSET_1, RELSET_1, RLVECT_1, XCMPLX_0, XCMPLX_1, ZFMISC_1, FUNCOP_1, SEQ_1, SEQ_2, NAT_1, SEQM_3, RELAT_1, FUNCT_1, VFUNCT_1, FUNCT_2, SEQ_4, NORMSP_1, LOPBAN_1, LOPBAN_2, LOPBAN_3, PARTFUN1, PARTFUN2, NFCONT_1, XREAL_1, COMPLEX1, XXREAL_0, ORDINAL1, VALUED_1, STRUCT_0, VALUED_0, VECTSP_1, NORMSP_0, NUMBERS;
schemes NAT_1, SEQ_1, RECDEF_1, FUNCT_2;
registrations FUNCT_1, ORDINAL1, RELSET_1, NUMBERS, XREAL_0, MEMBERED, FDIFF_1, STRUCT_0, LOPBAN_1, LOPBAN_2, VALUED_0, VALUED_1, FUNCT_2, FUNCOP_1, NAT_1;
constructors HIDDEN, REAL_1, SQUARE_1, COMPLEX1, SEQ_2, FDIFF_1, RSSPACE, VFUNCT_1, LOPBAN_3, NFCONT_1, RECDEF_1, RELSET_1, BINOP_2, RVSUM_1, COMSEQ_2, NUMBERS;
requirements HIDDEN, SUBSET, REAL, BOOLE, NUMERALS, ARITHM;
equalities XBOOLE_0, RLVECT_1, SUBSET_1, VALUED_1, STRUCT_0;
expansions TARSKI, XBOOLE_0, NFCONT_1, NORMSP_1, STRUCT_0;
definition
let S,
T be
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