begin
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 , ) ) )
theorem
:: deftheorem SEQFUNC:def 1 :
canceled;
:: deftheorem Def2 defines (#) SEQFUNC:def 2 :
definition
let D be non
empty set ;
let H be
Functional_Sequence of
D,
REAL ;
func H " -> Functional_Sequence of
D,
REAL means :
Def3:
for
n being
Nat holds
it . n = (H . n) ^ ;
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
func - H -> Functional_Sequence of
D,
REAL means :
Def4:
for
n being
Nat holds
it . n = - (H . n);
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
func abs H -> Functional_Sequence of
D,
REAL means :
Def5:
for
n being
Nat holds
it . n = abs (H . 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
end;
:: deftheorem Def3 defines " SEQFUNC:def 3 :
:: deftheorem Def4 defines - SEQFUNC:def 4 :
:: deftheorem Def5 defines abs SEQFUNC:def 5 :
:: deftheorem Def6 defines + SEQFUNC:def 6 :
:: deftheorem defines - SEQFUNC:def 7 :
:: deftheorem Def8 defines (#) SEQFUNC:def 8 :
:: deftheorem defines / SEQFUNC:def 9 :
theorem
canceled;
theorem
theorem Th4:
theorem
theorem Th6:
theorem
theorem Th8:
theorem
theorem
theorem Th11:
theorem Th12:
theorem
theorem
theorem
theorem Th16:
theorem Th17:
theorem
theorem
:: deftheorem Def10 defines common_on_dom SEQFUNC:def 10 :
:: deftheorem Def11 defines # SEQFUNC:def 11 :
:: deftheorem Def12 defines is_point_conv_on SEQFUNC:def 12 :
theorem Th20:
theorem Th21:
:: deftheorem Def13 defines is_unif_conv_on SEQFUNC:def 13 :
:: deftheorem Def14 defines lim SEQFUNC:def 14 :
theorem Th22:
theorem Th23:
theorem Th24:
theorem
theorem
theorem Th27:
theorem
theorem Th29:
theorem Th30:
theorem Th31:
theorem Th32:
theorem Th33:
theorem Th34:
theorem Th35:
theorem
theorem
theorem Th38:
theorem Th39:
theorem Th40:
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) )
theorem
theorem
theorem Th44:
theorem