environ
vocabularies HIDDEN, NUMBERS, SUBSET_1, REAL_1, XXREAL_0, CARD_1, ARYTM_1, ARYTM_3, COMPLEX1, RELAT_1, XBOOLE_0, FINSEQ_1, TARSKI, FUNCT_1, PARTFUN1, VALUED_1, CLASSES1, FUNCOP_1, MEMBERED, VALUED_0, ORDINAL4, BINOP_1, SETWISEO, CARD_3, NAT_1, RFINSEQ, FUNCT_3, PBOOLE, LIMFUNC1, FINSET_1, XXREAL_1, FINSEQ_2, RFUNCT_3, FUNCT_7;
notations HIDDEN, TARSKI, XBOOLE_0, SUBSET_1, ORDINAL1, CARD_1, NUMBERS, XCMPLX_0, XREAL_0, COMPLEX1, MEMBERED, RELAT_1, FUNCT_1, RELSET_1, PARTFUN1, FUNCT_2, BINOP_1, XXREAL_0, REAL_1, NAT_1, FUNCOP_1, SETWISEO, FINSEQ_2, FINSEQ_1, FINSEQOP, VALUED_0, VALUED_1, RFUNCT_1, FINSEQ_4, SETWOP_2, FINSET_1, RVSUM_1, RCOMP_1, PARTFUN2, LIMFUNC1, CLASSES1, RFINSEQ;
definitions TARSKI, BINOP_1, SETWISEO, RFINSEQ, XBOOLE_0;
theorems FINSEQ_1, FINSEQ_2, NAT_1, FUNCT_1, CARD_2, TARSKI, CARD_1, FINSET_1, PARTFUN1, RCOMP_1, BINOP_1, FINSEQ_3, FUNCOP_1, RFUNCT_1, ZFMISC_1, RVSUM_1, ABSVALUE, RFINSEQ, RELAT_1, FINSOP_1, XREAL_0, XBOOLE_0, XBOOLE_1, XCMPLX_0, XCMPLX_1, XREAL_1, COMPLEX1, XXREAL_0, VALUED_1, RELSET_1, XXREAL_1, CLASSES1;
schemes NAT_1, FINSEQ_1, SEQ_1, BINOP_1;
registrations XBOOLE_0, RELSET_1, PARTFUN1, FINSET_1, NUMBERS, XXREAL_0, XREAL_0, NAT_1, MEMBERED, FINSEQ_1, FINSEQ_2, VALUED_0, FUNCT_1, CARD_1, RVSUM_1, ORDINAL1;
constructors HIDDEN, PARTFUN1, BINOP_1, SETWISEO, REAL_1, NAT_1, BINOP_2, COMPLEX1, SEQM_3, PROB_1, SEQ_4, FINSEQOP, RCOMP_1, FINSEQ_4, FINSOP_1, PARTFUN2, RFUNCT_1, RVSUM_1, LIMFUNC1, RFINSEQ, CLASSES1, RELSET_1, SETFAM_1, VALUED_0, SQUARE_1;
requirements HIDDEN, REAL, NUMERALS, BOOLE, SUBSET, ARITHM;
equalities SUBSET_1, FINSEQ_2, RVSUM_1, LIMFUNC1, VALUED_1, RELAT_1;
expansions TARSKI, BINOP_1, XBOOLE_0, RELAT_1;
Lm1:
for n being Nat
for D being non empty set
for f being FinSequence of D st len f <= n holds
f | n = f
Lm2:
for f being Function
for x being set st not x in rng f holds
f " {x} = {}
definition
let D be non
empty set ;
let E be
real-membered set ;
let F1,
F2 be
Element of
PFuncs (
D,
E);
+redefine func F1 + F2 -> Element of
PFuncs (
D,
REAL);
coherence
F1 + F2 is Element of PFuncs (D,REAL)
-redefine func F1 - F2 -> Element of
PFuncs (
D,
REAL);
coherence
F1 - F2 is Element of PFuncs (D,REAL)
(#)redefine func F1 (#) F2 -> Element of
PFuncs (
D,
REAL);
coherence
F1 (#) F2 is Element of PFuncs (D,REAL)
/redefine func F1 / F2 -> Element of
PFuncs (
D,
REAL);
coherence
F1 / F2 is Element of PFuncs (D,REAL)
end;
definition
let D be non
empty set ;
existence
ex b1 being BinOp of (PFuncs (D,REAL)) st
for F1, F2 being Element of PFuncs (D,REAL) holds b1 . (F1,F2) = F1 + F2
uniqueness
for b1, b2 being BinOp of (PFuncs (D,REAL)) st ( for F1, F2 being Element of PFuncs (D,REAL) holds b1 . (F1,F2) = F1 + F2 ) & ( for F1, F2 being Element of PFuncs (D,REAL) holds b2 . (F1,F2) = F1 + F2 ) holds
b1 = b2
end;
definition
let D be non
empty set ;
let f be
FinSequence of
PFuncs (
D,
REAL);
let R be
FinSequence of
REAL ;
existence
ex b1 being FinSequence of PFuncs (D,REAL) st
( len b1 = min ((len R),(len f)) & ( for n being Nat st n in dom b1 holds
for F being PartFunc of D,REAL
for r being Real st r = R . n & F = f . n holds
b1 . n = r (#) F ) )
uniqueness
for b1, b2 being FinSequence of PFuncs (D,REAL) st len b1 = min ((len R),(len f)) & ( for n being Nat st n in dom b1 holds
for F being PartFunc of D,REAL
for r being Real st r = R . n & F = f . n holds
b1 . n = r (#) F ) & len b2 = min ((len R),(len f)) & ( for n being Nat st n in dom b2 holds
for F being PartFunc of D,REAL
for r being Real st r = R . n & F = f . n holds
b2 . n = r (#) F ) holds
b1 = b2
end;
defpred S1[ Nat] means for D being non empty set
for F being PartFunc of D,REAL
for X, Y being set
for Z being finite set st Z = dom (F | Y) & dom (F | X) is finite & Y c= X & $1 = card Z & ( for d1, d2 being Element of D st d1 in dom (F | Y) & d2 in dom (F | (X \ Y)) holds
F . d1 >= F . d2 ) holds
FinS (F,X) = (FinS (F,Y)) ^ (FinS (F,(X \ Y)));
Lm3:
S1[ 0 ]
Lm4:
for n being Nat st S1[n] holds
S1[n + 1]
:: Partial Functions from a Domain to the Set of Real Numbers
::