:: SEQFUNC semantic presentation  Show TPTP formulae Show IDV graph for whole article:: Showing IDV graph ... (Click the Palm Trees again to close it)

definition
let D1, D2 be set ;
mode Functional_Sequence of D1,D2 -> Function means :Def1: :: SEQFUNC:def 1
( dom it = NAT & rng it c= PFuncs D1,D2 );
existence
ex b1 being Function st
( dom b1 = NAT & rng b1 c= PFuncs D1,D2 )
proof end;
end;

:: deftheorem Def1 defines Functional_Sequence SEQFUNC:def 1 :
for D1, D2 being set
for b3 being Function holds
( b3 is Functional_Sequence of D1,D2 iff ( dom b3 = NAT & rng b3 c= PFuncs D1,D2 ) );

definition
let D1, D2 be set ;
let F be Functional_Sequence of D1,D2;
let n be natural number ;
:: original: .
redefine func F . n -> PartFunc of D1,D2;
coherence
F . n is PartFunc of D1,D2
proof end;
end;

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 ) ) )
proof end;

theorem :: SEQFUNC:1  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for D1, D2 being set
for f being Function holds
( f is Functional_Sequence of D1,D2 iff ( dom f = NAT & ( for n being Nat holds f . n is PartFunc of D1,D2 ) ) )
proof end;

Lm2: for D2, D1 being set
for F1, F2 being Functional_Sequence of D1,D2 st ( for x being set st x in NAT holds
F1 . x = F2 . x ) holds
F1 = F2
proof end;

theorem Th2: :: SEQFUNC:2  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for D2, D1 being set
for F1, F2 being Functional_Sequence of D1,D2 st ( for n being Nat holds F1 . n = F2 . n ) holds
F1 = F2
proof end;

scheme :: SEQFUNC:sch 1
ExFuncSeq{ F1() -> set , F2() -> set , F3( Nat) -> PartFunc of F1(),F2() } :
ex G being Functional_Sequence of F1(),F2() st
for n being Nat holds G . n = F3(n)
proof end;

definition
let D be non empty set ;
let H be Functional_Sequence of D, REAL ;
let r be real number ;
func r (#) H -> Functional_Sequence of D, REAL means :Def2: :: SEQFUNC:def 2
for n being Nat holds it . n = r (#) (H . n);
existence
ex b1 being Functional_Sequence of D, REAL st
for n being Nat holds b1 . n = r (#) (H . n)
proof end;
uniqueness
for b1, b2 being Functional_Sequence of D, REAL st ( for n being Nat holds b1 . n = r (#) (H . n) ) & ( for n being Nat holds b2 . n = r (#) (H . n) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def2 defines (#) SEQFUNC:def 2 :
for D being non empty set
for H being Functional_Sequence of D, REAL
for r being real number
for b4 being Functional_Sequence of D, REAL holds
( b4 = r (#) H iff for n being Nat holds b4 . n = r (#) (H . n) );

definition
let D be non empty set ;
let H be Functional_Sequence of D, REAL ;
func H " -> Functional_Sequence of D, REAL means :Def3: :: SEQFUNC:def 3
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) ^
proof end;
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
proof end;
func - H -> Functional_Sequence of D, REAL means :Def4: :: SEQFUNC:def 4
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)
proof end;
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
proof end;
func abs H -> Functional_Sequence of D, REAL means :Def5: :: SEQFUNC:def 5
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)
proof end;
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
proof end;
end;

:: deftheorem Def3 defines " SEQFUNC:def 3 :
for D being non empty set
for H, b3 being Functional_Sequence of D, REAL holds
( b3 = H " iff for n being Nat holds b3 . n = (H . n) ^ );

:: deftheorem Def4 defines - SEQFUNC:def 4 :
for D being non empty set
for H, b3 being Functional_Sequence of D, REAL holds
( b3 = - H iff for n being Nat holds b3 . n = - (H . n) );

:: deftheorem Def5 defines abs SEQFUNC:def 5 :
for D being non empty set
for H, b3 being Functional_Sequence of D, REAL holds
( b3 = abs H iff for n being Nat holds b3 . n = abs (H . n) );

definition
let D be non empty set ;
let G, H be Functional_Sequence of D, REAL ;
func G + H -> Functional_Sequence of D, REAL means :Def6: :: SEQFUNC:def 6
for n being Nat holds it . n = (G . n) + (H . n);
existence
ex b1 being Functional_Sequence of D, REAL st
for n being Nat holds b1 . n = (G . n) + (H . n)
proof end;
uniqueness
for b1, b2 being Functional_Sequence of D, REAL st ( for n being Nat holds b1 . n = (G . n) + (H . n) ) & ( for n being Nat holds b2 . n = (G . n) + (H . n) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def6 defines + SEQFUNC:def 6 :
for D being non empty set
for G, H, b4 being Functional_Sequence of D, REAL holds
( b4 = G + H iff for n being Nat holds b4 . n = (G . n) + (H . n) );

definition
let D be non empty set ;
let G, H be Functional_Sequence of D, REAL ;
func G - H -> Functional_Sequence of D, REAL equals :: SEQFUNC:def 7
G + (- H);
correctness
coherence
G + (- H) is Functional_Sequence of D, REAL ;
;
end;

:: deftheorem defines - SEQFUNC:def 7 :
for D being non empty set
for G, H being Functional_Sequence of D, REAL holds G - H = G + (- H);

definition
let D be non empty set ;
let G, H be Functional_Sequence of D, REAL ;
func G (#) H -> Functional_Sequence of D, REAL means :Def8: :: SEQFUNC:def 8
for n being Nat holds it . n = (G . n) (#) (H . n);
existence
ex b1 being Functional_Sequence of D, REAL st
for n being Nat holds b1 . n = (G . n) (#) (H . n)
proof end;
uniqueness
for b1, b2 being Functional_Sequence of D, REAL st ( for n being Nat holds b1 . n = (G . n) (#) (H . n) ) & ( for n being Nat holds b2 . n = (G . n) (#) (H . n) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def8 defines (#) SEQFUNC:def 8 :
for D being non empty set
for G, H, b4 being Functional_Sequence of D, REAL holds
( b4 = G (#) H iff for n being Nat holds b4 . n = (G . n) (#) (H . n) );

definition
let D be non empty set ;
let H, G be Functional_Sequence of D, REAL ;
func G / H -> Functional_Sequence of D, REAL equals :: SEQFUNC:def 9
G (#) (H " );
correctness
coherence
G (#) (H " ) is Functional_Sequence of D, REAL ;
;
end;

:: deftheorem defines / SEQFUNC:def 9 :
for D being non empty set
for H, G being Functional_Sequence of D, REAL holds G / H = G (#) (H " );

theorem :: SEQFUNC:3  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for D being non empty set
for H1, G, H being Functional_Sequence of D, REAL holds
( H1 = G / H iff for n being Nat holds H1 . n = (G . n) / (H . n) )
proof end;

theorem Th4: :: SEQFUNC:4  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for D being non empty set
for H1, G, H being Functional_Sequence of D, REAL holds
( H1 = G - H iff for n being Nat holds H1 . n = (G . n) - (H . n) )
proof end;

theorem :: SEQFUNC:5  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for D being non empty set
for G, H, J being Functional_Sequence of D, REAL holds
( G + H = H + G & (G + H) + J = G + (H + J) )
proof end;

theorem Th6: :: SEQFUNC:6  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for D being non empty set
for G, H, J being Functional_Sequence of D, REAL holds
( G (#) H = H (#) G & (G (#) H) (#) J = G (#) (H (#) J) )
proof end;

theorem :: SEQFUNC:7  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for D being non empty set
for G, H, J being Functional_Sequence of D, REAL holds
( (G + H) (#) J = (G (#) J) + (H (#) J) & J (#) (G + H) = (J (#) G) + (J (#) H) )
proof end;

theorem Th8: :: SEQFUNC:8  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for D being non empty set
for H being Functional_Sequence of D, REAL holds - H = (- 1) (#) H
proof end;

theorem :: SEQFUNC:9  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for D being non empty set
for G, H, J being Functional_Sequence of D, REAL holds
( (G - H) (#) J = (G (#) J) - (H (#) J) & (J (#) G) - (J (#) H) = J (#) (G - H) )
proof end;

theorem :: SEQFUNC:10  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for D being non empty set
for r being Real
for G, H being Functional_Sequence of D, REAL holds
( r (#) (G + H) = (r (#) G) + (r (#) H) & r (#) (G - H) = (r (#) G) - (r (#) H) )
proof end;

theorem Th11: :: SEQFUNC:11  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for D being non empty set
for r, p being Real
for H being Functional_Sequence of D, REAL holds (r * p) (#) H = r (#) (p (#) H)
proof end;

theorem Th12: :: SEQFUNC:12  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for D being non empty set
for H being Functional_Sequence of D, REAL holds 1 (#) H = H
proof end;

theorem :: SEQFUNC:13  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for D being non empty set
for H being Functional_Sequence of D, REAL holds - (- H) = H
proof end;

theorem :: SEQFUNC:14  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for D being non empty set
for G, H being Functional_Sequence of D, REAL holds (G " ) (#) (H " ) = (G (#) H) "
proof end;

theorem :: SEQFUNC:15  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for D being non empty set
for r being Real
for H being Functional_Sequence of D, REAL st r <> 0 holds
(r (#) H) " = (r " ) (#) (H " )
proof end;

theorem Th16: :: SEQFUNC:16  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for D being non empty set
for H being Functional_Sequence of D, REAL holds (abs H) " = abs (H " )
proof end;

theorem Th17: :: SEQFUNC:17  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for D being non empty set
for G, H being Functional_Sequence of D, REAL holds abs (G (#) H) = (abs G) (#) (abs H)
proof end;

theorem :: SEQFUNC:18  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for D being non empty set
for G, H being Functional_Sequence of D, REAL holds abs (G / H) = (abs G) / (abs H)
proof end;

theorem :: SEQFUNC:19  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for D being non empty set
for r being Real
for H being Functional_Sequence of D, REAL holds abs (r (#) H) = (abs r) (#) (abs H)
proof end;

definition
let D1, D2 be set ;
let F be Functional_Sequence of D1,D2;
let X be set ;
pred X common_on_dom F means :Def10: :: SEQFUNC:def 10
( X <> {} & ( for n being Nat holds X c= dom (F . n) ) );
end;

:: deftheorem Def10 defines common_on_dom SEQFUNC:def 10 :
for D1, D2 being set
for F being Functional_Sequence of D1,D2
for X being set holds
( X common_on_dom F iff ( X <> {} & ( for n being Nat holds X c= dom (F . n) ) ) );

definition
let D be non empty set ;
let H be Functional_Sequence of D, REAL ;
let x be Element of D;
func H # x -> Real_Sequence means :Def11: :: SEQFUNC:def 11
for n being Nat holds it . n = (H . n) . x;
existence
ex b1 being Real_Sequence st
for n being Nat holds b1 . n = (H . n) . x
proof end;
uniqueness
for b1, b2 being Real_Sequence st ( for n being Nat holds b1 . n = (H . n) . x ) & ( for n being Nat holds b2 . n = (H . n) . x ) holds
b1 = b2
proof end;
end;

:: deftheorem Def11 defines # SEQFUNC:def 11 :
for D being non empty set
for H being Functional_Sequence of D, REAL
for x being Element of D
for b4 being Real_Sequence holds
( b4 = H # x iff for n being Nat holds b4 . n = (H . n) . x );

definition
let D be non empty set ;
let H be Functional_Sequence of D, REAL ;
let X be set ;
pred H is_point_conv_on X means :Def12: :: SEQFUNC:def 12
( X common_on_dom H & ex f being PartFunc of D, REAL st
( X = dom f & ( for x being Element of D st x in X holds
for p being Real st p > 0 holds
ex k being Nat st
for n being Nat st n >= k holds
abs (((H . n) . x) - (f . x)) < p ) ) );
end;

:: deftheorem Def12 defines is_point_conv_on SEQFUNC:def 12 :
for D being non empty set
for H being Functional_Sequence of D, REAL
for X being set holds
( H is_point_conv_on X iff ( X common_on_dom H & ex f being PartFunc of D, REAL st
( X = dom f & ( for x being Element of D st x in X holds
for p being Real st p > 0 holds
ex k being Nat st
for n being Nat st n >= k holds
abs (((H . n) . x) - (f . x)) < p ) ) ) );

theorem Th20: :: SEQFUNC:20  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for D being non empty set
for H being Functional_Sequence of D, REAL
for X being set holds
( H is_point_conv_on X iff ( X common_on_dom H & ex f being PartFunc of D, REAL st
( X = dom f & ( for x being Element of D st x in X holds
( H # x is convergent & lim (H # x) = f . x ) ) ) ) )
proof end;

theorem Th21: :: SEQFUNC:21  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for D being non empty set
for H being Functional_Sequence of D, REAL
for X being set holds
( H is_point_conv_on X iff ( X common_on_dom H & ( for x being Element of D st x in X holds
H # x is convergent ) ) )
proof end;

definition
let D be non empty set ;
let H be Functional_Sequence of D, REAL ;
let X be set ;
pred H is_unif_conv_on X means :Def13: :: SEQFUNC:def 13
( X common_on_dom H & ex f being PartFunc of D, REAL st
( X = dom f & ( for p being Real st p > 0 holds
ex k being Nat st
for n being Nat
for x being Element of D st n >= k & x in X holds
abs (((H . n) . x) - (f . x)) < p ) ) );
end;

:: deftheorem Def13 defines is_unif_conv_on SEQFUNC:def 13 :
for D being non empty set
for H being Functional_Sequence of D, REAL
for X being set holds
( H is_unif_conv_on X iff ( X common_on_dom H & ex f being PartFunc of D, REAL st
( X = dom f & ( for p being Real st p > 0 holds
ex k being Nat st
for n being Nat
for x being Element of D st n >= k & x in X holds
abs (((H . n) . x) - (f . x)) < p ) ) ) );

definition
let D be non empty set ;
let H be Functional_Sequence of D, REAL ;
let X be set ;
assume A1: H is_point_conv_on X ;
func lim H,X -> PartFunc of D, REAL means :Def14: :: SEQFUNC:def 14
( dom it = X & ( for x being Element of D st x in dom it holds
it . x = lim (H # x) ) );
existence
ex b1 being PartFunc of D, REAL st
( dom b1 = X & ( for x being Element of D st x in dom b1 holds
b1 . x = lim (H # x) ) )
proof end;
uniqueness
for b1, b2 being PartFunc of D, REAL st dom b1 = X & ( for x being Element of D st x in dom b1 holds
b1 . x = lim (H # x) ) & dom b2 = X & ( for x being Element of D st x in dom b2 holds
b2 . x = lim (H # x) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def14 defines lim SEQFUNC:def 14 :
for D being non empty set
for H being Functional_Sequence of D, REAL
for X being set st H is_point_conv_on X holds
for b4 being PartFunc of D, REAL holds
( b4 = lim H,X iff ( dom b4 = X & ( for x being Element of D st x in dom b4 holds
b4 . x = lim (H # x) ) ) );

theorem Th22: :: SEQFUNC:22  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for D being non empty set
for H being Functional_Sequence of D, REAL
for X being set
for f being PartFunc of D, REAL st H is_point_conv_on X holds
( f = lim H,X iff ( dom f = X & ( for x being Element of D st x in X holds
for p being Real st p > 0 holds
ex k being Nat st
for n being Nat st n >= k holds
abs (((H . n) . x) - (f . x)) < p ) ) )
proof end;

theorem Th23: :: SEQFUNC:23  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for D being non empty set
for H being Functional_Sequence of D, REAL
for X being set st H is_unif_conv_on X holds
H is_point_conv_on X
proof end;

theorem Th24: :: SEQFUNC:24  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for D being non empty set
for H being Functional_Sequence of D, REAL
for Y, X being set st Y c= X & Y <> {} & X common_on_dom H holds
Y common_on_dom H
proof end;

theorem :: SEQFUNC:25  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for D being non empty set
for H being Functional_Sequence of D, REAL
for Y, X being set st Y c= X & Y <> {} & H is_point_conv_on X holds
( H is_point_conv_on Y & (lim H,X) | Y = lim H,Y )
proof end;

theorem :: SEQFUNC:26  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for D being non empty set
for H being Functional_Sequence of D, REAL
for Y, X being set st Y c= X & Y <> {} & H is_unif_conv_on X holds
H is_unif_conv_on Y
proof end;

theorem Th27: :: SEQFUNC:27  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for D being non empty set
for H being Functional_Sequence of D, REAL
for X being set st X common_on_dom H holds
for x being Element of D st x in X holds
{x} common_on_dom H
proof end;

theorem :: SEQFUNC:28  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for D being non empty set
for H being Functional_Sequence of D, REAL
for X being set st H is_point_conv_on X holds
for x being Element of D st x in X holds
{x} common_on_dom H
proof end;

theorem Th29: :: SEQFUNC:29  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for D being non empty set
for H1, H2 being Functional_Sequence of D, REAL
for x being Element of D st {x} common_on_dom H1 & {x} common_on_dom H2 holds
( (H1 # x) + (H2 # x) = (H1 + H2) # x & (H1 # x) - (H2 # x) = (H1 - H2) # x & (H1 # x) (#) (H2 # x) = (H1 (#) H2) # x )
proof end;

theorem Th30: :: SEQFUNC:30  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for D being non empty set
for H being Functional_Sequence of D, REAL
for x being Element of D st {x} common_on_dom H holds
( (abs H) # x = abs (H # x) & (- H) # x = - (H # x) )
proof end;

theorem Th31: :: SEQFUNC:31  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for D being non empty set
for r being Real
for H being Functional_Sequence of D, REAL
for x being Element of D st {x} common_on_dom H holds
(r (#) H) # x = r (#) (H # x)
proof end;

theorem Th32: :: SEQFUNC:32  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for D being non empty set
for H1, H2 being Functional_Sequence of D, REAL
for X being set st X common_on_dom H1 & X common_on_dom H2 holds
for x being Element of D st x in X holds
( (H1 # x) + (H2 # x) = (H1 + H2) # x & (H1 # x) - (H2 # x) = (H1 - H2) # x & (H1 # x) (#) (H2 # x) = (H1 (#) H2) # x )
proof end;

theorem Th33: :: SEQFUNC:33  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for D being non empty set
for H being Functional_Sequence of D, REAL
for X being set st X common_on_dom H holds
for x being Element of D st x in X holds
( (abs H) # x = abs (H # x) & (- H) # x = - (H # x) )
proof end;

theorem Th34: :: SEQFUNC:34  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for D being non empty set
for r being Real
for H being Functional_Sequence of D, REAL
for X being set st X common_on_dom H holds
for x being Element of D st x in X holds
(r (#) H) # x = r (#) (H # x)
proof end;

theorem Th35: :: SEQFUNC:35  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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
for x being Element of D st x in X holds
( (H1 # x) + (H2 # x) = (H1 + H2) # x & (H1 # x) - (H2 # x) = (H1 - H2) # x & (H1 # x) (#) (H2 # x) = (H1 (#) H2) # x )
proof end;

theorem Th36: :: SEQFUNC:36  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for D being non empty set
for H being Functional_Sequence of D, REAL
for X being set st H is_point_conv_on X holds
for x being Element of D st x in X holds
( (abs H) # x = abs (H # x) & (- H) # x = - (H # x) )
proof end;

theorem :: SEQFUNC:37  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for D being non empty set
for r being Real
for H being Functional_Sequence of D, REAL
for X being set st H is_point_conv_on X holds
for x being Element of D st x in X holds
(r (#) H) # x = r (#) (H # x)
proof end;

theorem Th38: :: SEQFUNC:38  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for D being non empty set
for H1, H2 being Functional_Sequence of D, REAL
for X being set st X common_on_dom H1 & X common_on_dom H2 holds
( X common_on_dom H1 + H2 & X common_on_dom H1 - H2 & X common_on_dom H1 (#) H2 )
proof end;

theorem Th39: :: SEQFUNC:39  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for D being non empty set
for H being Functional_Sequence of D, REAL
for X being set st X common_on_dom H holds
( X common_on_dom abs H & X common_on_dom - H )
proof end;

theorem Th40: :: SEQFUNC:40  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for D being non empty set
for r being Real
for H being Functional_Sequence of D, REAL
for X being set st X common_on_dom H holds
X common_on_dom r (#) H
proof end;

theorem :: SEQFUNC:41  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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) )
proof end;

theorem :: SEQFUNC:42  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for D being non empty set
for H being Functional_Sequence of D, REAL
for X being set st H is_point_conv_on X holds
( abs H is_point_conv_on X & lim (abs H),X = abs (lim H,X) & - H is_point_conv_on X & lim (- H),X = - (lim H,X) )
proof end;

theorem :: SEQFUNC:43  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for D being non empty set
for r being Real
for H being Functional_Sequence of D, REAL
for X being set st H is_point_conv_on X holds
( r (#) H is_point_conv_on X & lim (r (#) H),X = r (#) (lim H,X) )
proof end;

theorem Th44: :: SEQFUNC:44  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for D being non empty set
for H being Functional_Sequence of D, REAL
for X being set holds
( H is_unif_conv_on X iff ( X common_on_dom H & H is_point_conv_on X & ( for r being Real st 0 < r holds
ex k being Nat st
for n being Nat
for x being Element of D st n >= k & x in X holds
abs (((H . n) . x) - ((lim H,X) . x)) < r ) ) )
proof end;

theorem :: SEQFUNC:45  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being set
for H being Functional_Sequence of REAL , REAL st H is_unif_conv_on X & ( for n being Nat holds H . n is_continuous_on X ) holds
lim H,X is_continuous_on X
proof end;