environ
vocabularies HIDDEN, NUMBERS, REAL_1, NORMSP_1, PRE_TOPC, PARTFUN1, FUNCT_1, NAT_1, FDIFF_1, SUBSET_1, RELAT_1, LOPBAN_1, RCOMP_1, TARSKI, SEQ_1, ARYTM_3, VALUED_1, FUNCT_2, ARYTM_1, SEQ_2, ORDINAL2, SUPINF_2, FCONT_1, COMPLEX1, STRUCT_0, CARD_1, VALUED_0, XXREAL_0, FUNCOP_1, XBOOLE_0, CARD_3, FINSEQ_1, FINSEQ_2, BORSUK_1, REAL_NS1, RLVECT_1, SQUARE_1, RVSUM_1, XXREAL_1, PDIFF_1, EUCLID, RFINSEQ2, FUNCT_7, XCMPLX_0;
notations HIDDEN, TARSKI, XBOOLE_0, SUBSET_1, RELAT_1, FUNCT_1, ORDINAL1, RELSET_1, PARTFUN1, FUNCT_2, FUNCOP_1, NUMBERS, XXREAL_0, XXREAL_3, EXTREAL1, XCMPLX_0, XREAL_0, REAL_1, SQUARE_1, NAT_1, VALUED_0, FINSEQ_1, VALUED_1, FINSEQ_2, SEQ_1, SEQ_2, FINSEQOP, RVSUM_1, RCOMP_1, FDIFF_1, COMPLEX1, RFINSEQ2, STRUCT_0, PRE_TOPC, RLVECT_1, VFUNCT_1, NORMSP_0, NORMSP_1, EUCLID, LOPBAN_1, NFCONT_1, NDIFF_1, REAL_NS1, PDIFF_1, INTEGR15, PDIFF_6, NFCONT_3, NDIFF_3, NFCONT_4, PDIFF_7;
definitions TARSKI, NFCONT_1;
theorems TARSKI, ABSVALUE, XBOOLE_0, XBOOLE_1, RLVECT_1, XCMPLX_0, XCMPLX_1, SEQ_1, SEQ_2, NAT_1, RELAT_1, FUNCT_1, VFUNCT_1, FUNCT_2, ORDINAL1, SEQ_4, NORMSP_1, LOPBAN_1, PARTFUN1, PARTFUN2, NFCONT_1, FDIFF_1, NDIFF_1, FUNCOP_1, XREAL_1, COMPLEX1, XXREAL_0, VALUED_1, VALUED_0, VECTSP_1, NORMSP_0, XREAL_0, RCOMP_1, FINSEQ_1, FINSEQ_2, RVSUM_1, FRECHET, REAL_NS1, SQUARE_1, PDIFF_1, JORDAN2C, RLVECT_4, EUCLID, PDIFF_6, RFINSEQ2, NFCONT_3, NDIFF_3, NFCONT_4, NDIFF_2, VALUED_2;
schemes FUNCT_2, SEQ_1, RECDEF_1;
registrations RELSET_1, STRUCT_0, ORDINAL1, XREAL_0, MEMBERED, FUNCT_1, FUNCT_2, NUMBERS, XBOOLE_0, VALUED_0, EUCLID, NORMSP_0, NORMSP_1, XXREAL_0, LOPBAN_1, NAT_1, PDIFF_1, RCOMP_1, VALUED_1, FDIFF_1, NDIFF_1, NDIFF_3, REAL_NS1, FCONT_3, VALUED_2, SQUARE_1, RVSUM_1;
constructors HIDDEN, REAL_1, SQUARE_1, COMPLEX1, SEQ_2, FDIFF_1, RSSPACE, VFUNCT_1, NFCONT_1, NDIFF_1, RELSET_1, EXTREAL1, RVSUM_1, BINOP_2, PDIFF_1, INTEGR15, JORDAN2B, FINSEQOP, RFINSEQ2, PDIFF_6, PDIFF_7, NFCONT_3, NDIFF_3, NFCONT_4, VALUED_2, COMSEQ_2, SEQ_1, NUMBERS;
requirements HIDDEN, SUBSET, REAL, BOOLE, NUMERALS, ARITHM;
equalities RLVECT_1, LOPBAN_1, EUCLID, PDIFF_1, RFINSEQ2, SQUARE_1, FINSEQ_1, RVSUM_1, XCMPLX_0, PDIFF_7, VALUED_1, SUBSET_1, STRUCT_0, INTEGR15;
expansions TARSKI, PDIFF_7, NFCONT_1;
set ZR = [#] REAL;
Lm1:
the carrier of (REAL-NS 1) = REAL 1
by REAL_NS1:def 4;
reconsider jj = 1 as Element of REAL by XREAL_0:def 1;
Lm2:
( dom (proj (1,1)) = REAL 1 & rng (proj (1,1)) = REAL & ( for x being Element of REAL holds
( (proj (1,1)) . <*x*> = x & ((proj (1,1)) ") . x = <*x*> ) ) )
definition
let n be non
zero Element of
NAT ;
let f be
PartFunc of
(REAL-NS n),
REAL;
let x be
Point of
(REAL-NS n);
existence
ex b1 being Function of (REAL-NS n),REAL ex g being PartFunc of (REAL n),REAL ex y being Element of REAL n st
( f = g & x = y & b1 = diff (g,y) )
uniqueness
for b1, b2 being Function of (REAL-NS n),REAL st ex g being PartFunc of (REAL n),REAL ex y being Element of REAL n st
( f = g & x = y & b1 = diff (g,y) ) & ex g being PartFunc of (REAL n),REAL ex y being Element of REAL n st
( f = g & x = y & b2 = diff (g,y) ) holds
b1 = b2
;
end;