environ
vocabularies HIDDEN, XBOOLE_0, SUBSET_1, NUMBERS, REAL_1, FUNCT_1, NAT_1, PARTFUN1, RELAT_1, TARSKI, VALUED_1, ORDINAL4, ARYTM_1, COMPLEX1, ARYTM_3, CARD_1, SEQ_1, PBOOLE, XXREAL_0, SEQ_2, ORDINAL2, FCONT_1, SEQFUNC, FUNCT_7, ORDINAL1;
notations HIDDEN, TARSKI, XBOOLE_0, SUBSET_1, ORDINAL1, NUMBERS, XCMPLX_0, XXREAL_0, XREAL_0, COMPLEX1, REAL_1, NAT_1, RELAT_1, FUNCT_1, RELSET_1, PARTFUN1, RFUNCT_1, VALUED_1, SEQ_1, COMSEQ_2, SEQ_2, FCONT_1;
definitions TARSKI, XBOOLE_0;
theorems FUNCT_1, PARTFUN1, TARSKI, RFUNCT_1, SEQ_1, SEQ_2, SEQ_4, ZFMISC_1, RFUNCT_2, FCONT_1, FUNCT_2, RELAT_1, XREAL_0, XBOOLE_0, XBOOLE_1, XREAL_1, COMPLEX1, XXREAL_0, ORDINAL1, VALUED_1, RELSET_1;
schemes CLASSES1, SEQ_1;
registrations XBOOLE_0, RELSET_1, NUMBERS, XREAL_0, MEMBERED, VALUED_0, VALUED_1, FUNCT_2, PARTFUN1, NAT_1;
constructors HIDDEN, PARTFUN1, FUNCOP_1, REAL_1, COMPLEX1, SEQ_2, RFUNCT_1, FCONT_1, LIMFUNC1, VALUED_1, RELSET_1, COMSEQ_2;
requirements HIDDEN, NUMERALS, SUBSET, BOOLE, ARITHM;
equalities VALUED_1;
expansions TARSKI;
Lm1:
for D1, D2 being set
for f being Function holds
( f is Functional_Sequence of D1,D2 iff ( dom f = NAT & ( for x being set st x in NAT holds
f . x is PartFunc of D1,D2 ) ) )
definition
let D be non
empty set ;
let H be
Functional_Sequence of
D,
REAL;
existence
ex b1 being Functional_Sequence of D,REAL st
for n being Nat holds b1 . n = (H . n) ^
uniqueness
for b1, b2 being Functional_Sequence of D,REAL st ( for n being Nat holds b1 . n = (H . n) ^ ) & ( for n being Nat holds b2 . n = (H . n) ^ ) holds
b1 = b2
existence
ex b1 being Functional_Sequence of D,REAL st
for n being Nat holds b1 . n = - (H . n)
uniqueness
for b1, b2 being Functional_Sequence of D,REAL st ( for n being Nat holds b1 . n = - (H . n) ) & ( for n being Nat holds b2 . n = - (H . n) ) holds
b1 = b2
involutiveness
for b1, b2 being Functional_Sequence of D,REAL st ( for n being Nat holds b1 . n = - (b2 . n) ) holds
for n being Nat holds b2 . n = - (b1 . n)
existence
ex b1 being Functional_Sequence of D,REAL st
for n being Nat holds b1 . n = abs (H . n)
uniqueness
for b1, b2 being Functional_Sequence of D,REAL st ( for n being Nat holds b1 . n = abs (H . n) ) & ( for n being Nat holds b2 . n = abs (H . n) ) holds
b1 = b2
projectivity
for b1, b2 being Functional_Sequence of D,REAL st ( for n being Nat holds b1 . n = abs (b2 . n) ) holds
for n being Nat holds b1 . n = abs (b1 . n)
end;
theorem
for
D being non
empty set for
H1,
H2 being
Functional_Sequence of
D,
REAL for
X being
set st
H1 is_point_conv_on X &
H2 is_point_conv_on X holds
(
H1 + H2 is_point_conv_on X &
lim (
(H1 + H2),
X)
= (lim (H1,X)) + (lim (H2,X)) &
H1 - H2 is_point_conv_on X &
lim (
(H1 - H2),
X)
= (lim (H1,X)) - (lim (H2,X)) &
H1 (#) H2 is_point_conv_on X &
lim (
(H1 (#) H2),
X)
= (lim (H1,X)) (#) (lim (H2,X)) )