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 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)) )