:: by Beata Perkowska

::

:: Received May 22, 1992

:: Copyright (c) 1992-2021 Association of Mizar Users

definition
end;

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

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

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

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

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;

definition

let D be non empty set ;

let H be Functional_Sequence of D,REAL;

let r be Real;

ex b_{1} being Functional_Sequence of D,REAL st

for n being Nat holds b_{1} . n = r (#) (H . n)

for b_{1}, b_{2} being Functional_Sequence of D,REAL st ( for n being Nat holds b_{1} . n = r (#) (H . n) ) & ( for n being Nat holds b_{2} . n = r (#) (H . n) ) holds

b_{1} = b_{2}

end;
let H be Functional_Sequence of D,REAL;

let r be Real;

func r (#) H -> Functional_Sequence of D,REAL means :Def1: :: SEQFUNC:def 1

for n being Nat holds it . n = r (#) (H . n);

existence for n being Nat holds it . n = r (#) (H . n);

ex b

for n being Nat holds b

proof end;

uniqueness for b

b

proof end;

:: deftheorem Def1 defines (#) SEQFUNC:def 1 :

for D being non empty set

for H being Functional_Sequence of D,REAL

for r being Real

for b_{4} being Functional_Sequence of D,REAL holds

( b_{4} = r (#) H iff for n being Nat holds b_{4} . n = r (#) (H . n) );

for D being non empty set

for H being Functional_Sequence of D,REAL

for r being Real

for b

( b

definition

let D be non empty set ;

let H be Functional_Sequence of D,REAL;

ex b_{1} being Functional_Sequence of D,REAL st

for n being Nat holds b_{1} . n = (H . n) ^

for b_{1}, b_{2} being Functional_Sequence of D,REAL st ( for n being Nat holds b_{1} . n = (H . n) ^ ) & ( for n being Nat holds b_{2} . n = (H . n) ^ ) holds

b_{1} = b_{2}

ex b_{1} being Functional_Sequence of D,REAL st

for n being Nat holds b_{1} . n = - (H . n)

for b_{1}, b_{2} being Functional_Sequence of D,REAL st ( for n being Nat holds b_{1} . n = - (H . n) ) & ( for n being Nat holds b_{2} . n = - (H . n) ) holds

b_{1} = b_{2}

for b_{1}, b_{2} being Functional_Sequence of D,REAL st ( for n being Nat holds b_{1} . n = - (b_{2} . n) ) holds

for n being Nat holds b_{2} . n = - (b_{1} . n)

ex b_{1} being Functional_Sequence of D,REAL st

for n being Nat holds b_{1} . n = abs (H . n)

for b_{1}, b_{2} being Functional_Sequence of D,REAL st ( for n being Nat holds b_{1} . n = abs (H . n) ) & ( for n being Nat holds b_{2} . n = abs (H . n) ) holds

b_{1} = b_{2}

for b_{1}, b_{2} being Functional_Sequence of D,REAL st ( for n being Nat holds b_{1} . n = abs (b_{2} . n) ) holds

for n being Nat holds b_{1} . n = abs (b_{1} . n)

end;
let H be Functional_Sequence of D,REAL;

func H " -> Functional_Sequence of D,REAL means :Def2: :: SEQFUNC:def 2

for n being Nat holds it . n = (H . n) ^ ;

existence for n being Nat holds it . n = (H . n) ^ ;

ex b

for n being Nat holds b

proof end;

uniqueness for b

b

proof end;

func - H -> Functional_Sequence of D,REAL means :Def3: :: SEQFUNC:def 3

for n being Nat holds it . n = - (H . n);

existence for n being Nat holds it . n = - (H . n);

ex b

for n being Nat holds b

proof end;

uniqueness for b

b

proof end;

involutiveness for b

for n being Nat holds b

proof end;

func abs H -> Functional_Sequence of D,REAL means :Def4: :: SEQFUNC:def 4

for n being Nat holds it . n = abs (H . n);

existence for n being Nat holds it . n = abs (H . n);

ex b

for n being Nat holds b

proof end;

uniqueness for b

b

proof end;

projectivity for b

for n being Nat holds b

proof end;

:: deftheorem Def2 defines " SEQFUNC:def 2 :

for D being non empty set

for H, b_{3} being Functional_Sequence of D,REAL holds

( b_{3} = H " iff for n being Nat holds b_{3} . n = (H . n) ^ );

for D being non empty set

for H, b

( b

:: deftheorem Def3 defines - SEQFUNC:def 3 :

for D being non empty set

for H, b_{3} being Functional_Sequence of D,REAL holds

( b_{3} = - H iff for n being Nat holds b_{3} . n = - (H . n) );

for D being non empty set

for H, b

( b

:: deftheorem Def4 defines abs SEQFUNC:def 4 :

for D being non empty set

for H, b_{3} being Functional_Sequence of D,REAL holds

( b_{3} = abs H iff for n being Nat holds b_{3} . n = abs (H . n) );

for D being non empty set

for H, b

( b

definition

let D be non empty set ;

let G, H be Functional_Sequence of D,REAL;

ex b_{1} being Functional_Sequence of D,REAL st

for n being Nat holds b_{1} . n = (G . n) + (H . n)

for b_{1}, b_{2} being Functional_Sequence of D,REAL st ( for n being Nat holds b_{1} . n = (G . n) + (H . n) ) & ( for n being Nat holds b_{2} . n = (G . n) + (H . n) ) holds

b_{1} = b_{2}

end;
let G, H be Functional_Sequence of D,REAL;

func G + H -> Functional_Sequence of D,REAL means :Def5: :: SEQFUNC:def 5

for n being Nat holds it . n = (G . n) + (H . n);

existence for n being Nat holds it . n = (G . n) + (H . n);

ex b

for n being Nat holds b

proof end;

uniqueness for b

b

proof end;

:: deftheorem Def5 defines + SEQFUNC:def 5 :

for D being non empty set

for G, H, b_{4} being Functional_Sequence of D,REAL holds

( b_{4} = G + H iff for n being Nat holds b_{4} . n = (G . n) + (H . n) );

for D being non empty set

for G, H, b

( b

definition

let D be non empty set ;

let G, H be Functional_Sequence of D,REAL;

correctness

coherence

G + (- H) is Functional_Sequence of D,REAL;

;

end;
let G, H be Functional_Sequence of D,REAL;

correctness

coherence

G + (- H) is Functional_Sequence of D,REAL;

;

:: deftheorem defines - SEQFUNC:def 6 :

for D being non empty set

for G, H being Functional_Sequence of D,REAL holds G - H = G + (- H);

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;

ex b_{1} being Functional_Sequence of D,REAL st

for n being Nat holds b_{1} . n = (G . n) (#) (H . n)

for b_{1}, b_{2} being Functional_Sequence of D,REAL st ( for n being Nat holds b_{1} . n = (G . n) (#) (H . n) ) & ( for n being Nat holds b_{2} . n = (G . n) (#) (H . n) ) holds

b_{1} = b_{2}

end;
let G, H be Functional_Sequence of D,REAL;

func G (#) H -> Functional_Sequence of D,REAL means :Def7: :: SEQFUNC:def 7

for n being Nat holds it . n = (G . n) (#) (H . n);

existence for n being Nat holds it . n = (G . n) (#) (H . n);

ex b

for n being Nat holds b

proof end;

uniqueness for b

b

proof end;

:: deftheorem Def7 defines (#) SEQFUNC:def 7 :

for D being non empty set

for G, H, b_{4} being Functional_Sequence of D,REAL holds

( b_{4} = G (#) H iff for n being Nat holds b_{4} . n = (G . n) (#) (H . n) );

for D being non empty set

for G, H, b

( b

definition

let D be non empty set ;

let H, G be Functional_Sequence of D,REAL;

correctness

coherence

G (#) (H ") is Functional_Sequence of D,REAL;

;

end;
let H, G be Functional_Sequence of D,REAL;

correctness

coherence

G (#) (H ") is Functional_Sequence of D,REAL;

;

:: deftheorem defines / SEQFUNC:def 8 :

for D being non empty set

for H, G being Functional_Sequence of D,REAL holds G / H = G (#) (H ");

for D being non empty set

for H, G being Functional_Sequence of D,REAL holds G / H = G (#) (H ");

theorem :: SEQFUNC:2

for D being non empty set

for G, H, H1 being Functional_Sequence of D,REAL holds

( H1 = G / H iff for n being Nat holds H1 . n = (G . n) / (H . n) )

for G, H, H1 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 Th3: :: SEQFUNC:3

for D being non empty set

for G, H, H1 being Functional_Sequence of D,REAL holds

( H1 = G - H iff for n being Nat holds H1 . n = (G . n) - (H . n) )

for G, H, H1 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:4

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

for G, H, J being Functional_Sequence of D,REAL holds

( G + H = H + G & (G + H) + J = G + (H + J) )

proof end;

theorem Th5: :: SEQFUNC:5

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

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:6

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

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 :: SEQFUNC:8

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

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:9

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

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 :: SEQFUNC:10

for D being non empty set

for p, r being Real

for H being Functional_Sequence of D,REAL holds (r * p) (#) H = r (#) (p (#) H)

for p, r being Real

for H being Functional_Sequence of D,REAL holds (r * p) (#) H = r (#) (p (#) H)

proof end;

::$CT

theorem :: SEQFUNC:13

for D being non empty set

for G, H being Functional_Sequence of D,REAL holds (G ") (#) (H ") = (G (#) H) "

for G, H being Functional_Sequence of D,REAL holds (G ") (#) (H ") = (G (#) H) "

proof end;

theorem :: SEQFUNC:14

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

for r being Real

for H being Functional_Sequence of D,REAL st r <> 0 holds

(r (#) H) " = (r ") (#) (H ")

proof end;

theorem Th15: :: SEQFUNC:16

for D being non empty set

for G, H being Functional_Sequence of D,REAL holds abs (G (#) H) = (abs G) (#) (abs H)

for G, H being Functional_Sequence of D,REAL holds abs (G (#) H) = (abs G) (#) (abs H)

proof end;

theorem :: SEQFUNC:17

for D being non empty set

for G, H being Functional_Sequence of D,REAL holds abs (G / H) = (abs G) / (abs H)

for G, H being Functional_Sequence of D,REAL holds abs (G / H) = (abs G) / (abs H)

proof end;

theorem :: SEQFUNC:18

for D being non empty set

for r being Real

for H being Functional_Sequence of D,REAL holds abs (r (#) H) = |.r.| (#) (abs H)

for r being Real

for H being Functional_Sequence of D,REAL holds abs (r (#) H) = |.r.| (#) (abs H)

proof end;

definition

let D1, D2 be set ;

let F be Functional_Sequence of D1,D2;

let X be set ;

end;
let F be Functional_Sequence of D1,D2;

let X be set ;

pred X common_on_dom F means :: SEQFUNC:def 9

( X <> {} & ( for n being Nat holds X c= dom (F . n) ) );

( X <> {} & ( for n being Nat holds X c= dom (F . n) ) );

:: deftheorem defines common_on_dom SEQFUNC:def 9 :

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

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;

ex b_{1} being Real_Sequence st

for n being Nat holds b_{1} . n = (H . n) . x

for b_{1}, b_{2} being Real_Sequence st ( for n being Nat holds b_{1} . n = (H . n) . x ) & ( for n being Nat holds b_{2} . n = (H . n) . x ) holds

b_{1} = b_{2}

end;
let H be Functional_Sequence of D,REAL;

let x be Element of D;

func H # x -> Real_Sequence means :Def10: :: SEQFUNC:def 10

for n being Nat holds it . n = (H . n) . x;

existence for n being Nat holds it . n = (H . n) . x;

ex b

for n being Nat holds b

proof end;

uniqueness for b

b

proof end;

:: deftheorem Def10 defines # SEQFUNC:def 10 :

for D being non empty set

for H being Functional_Sequence of D,REAL

for x being Element of D

for b_{4} being Real_Sequence holds

( b_{4} = H # x iff for n being Nat holds b_{4} . n = (H . n) . x );

for D being non empty set

for H being Functional_Sequence of D,REAL

for x being Element of D

for b

( b

:: deftheorem defines is_point_conv_on SEQFUNC:def 11 :

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

|.(((H . n) . x) - (f . x)).| < p ) ) ) );

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

|.(((H . n) . x) - (f . x)).| < p ) ) ) );

theorem Th18: :: SEQFUNC:19

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

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 Th19: :: SEQFUNC:20

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

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;

:: deftheorem defines is_unif_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_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

|.(((H . n) . x) - (f . x)).| < p ) ) ) );

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

|.(((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 ;

ex b_{1} being PartFunc of D,REAL st

( dom b_{1} = X & ( for x being Element of D st x in dom b_{1} holds

b_{1} . x = lim (H # x) ) )

for b_{1}, b_{2} being PartFunc of D,REAL st dom b_{1} = X & ( for x being Element of D st x in dom b_{1} holds

b_{1} . x = lim (H # x) ) & dom b_{2} = X & ( for x being Element of D st x in dom b_{2} holds

b_{2} . x = lim (H # x) ) holds

b_{1} = b_{2}

end;
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 :Def13: :: SEQFUNC:def 13

( dom it = X & ( for x being Element of D st x in dom it holds

it . x = lim (H # x) ) );

existence ( dom it = X & ( for x being Element of D st x in dom it holds

it . x = lim (H # x) ) );

ex b

( dom b

b

proof end;

uniqueness for b

b

b

b

proof end;

:: deftheorem Def13 defines lim SEQFUNC:def 13 :

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 b_{4} being PartFunc of D,REAL holds

( b_{4} = lim (H,X) iff ( dom b_{4} = X & ( for x being Element of D st x in dom b_{4} holds

b_{4} . x = lim (H # x) ) ) );

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 b

( b

b

theorem Th20: :: SEQFUNC:21

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

|.(((H . n) . x) - (f . x)).| < p ) ) )

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

|.(((H . n) . x) - (f . x)).| < p ) ) )

proof end;

theorem Th21: :: SEQFUNC:22

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

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 Th22: :: SEQFUNC:23

for D being non empty set

for H being Functional_Sequence of D,REAL

for X, Y being set st Y c= X & Y <> {} & X common_on_dom H holds

Y common_on_dom H

for H being Functional_Sequence of D,REAL

for X, Y being set st Y c= X & Y <> {} & X common_on_dom H holds

Y common_on_dom H

proof end;

theorem :: SEQFUNC:24

for D being non empty set

for H being Functional_Sequence of D,REAL

for X, Y 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) )

for H being Functional_Sequence of D,REAL

for X, Y 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:25

for D being non empty set

for H being Functional_Sequence of D,REAL

for X, Y being set st Y c= X & Y <> {} & H is_unif_conv_on X holds

H is_unif_conv_on Y

for H being Functional_Sequence of D,REAL

for X, Y being set st Y c= X & Y <> {} & H is_unif_conv_on X holds

H is_unif_conv_on Y

proof end;

theorem Th25: :: SEQFUNC:26

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

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:27

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 by Th25;

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 by Th25;

theorem Th27: :: SEQFUNC:28

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 )

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 Th28: :: SEQFUNC:29

for D being non empty set

for H being Functional_Sequence of D,REAL

for x being Element of D holds

( (abs H) # x = abs (H # x) & (- H) # x = - (H # x) )

for H being Functional_Sequence of D,REAL

for x being Element of D holds

( (abs H) # x = abs (H # x) & (- H) # x = - (H # x) )

proof end;

theorem Th29: :: SEQFUNC:30

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)

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 Th30: :: SEQFUNC:31

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 )

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 Th32: :: SEQFUNC:33

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)

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 Th33: :: SEQFUNC:34

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 ) by Th30;

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 ) by Th30;

theorem :: SEQFUNC:35

theorem :: SEQFUNC:36

theorem Th36: :: SEQFUNC:37

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 )

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 Th37: :: SEQFUNC:38

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 )

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 Th38: :: SEQFUNC:39

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

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:40

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

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:41

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) = |.(lim (H,X)).| & - H is_point_conv_on X & lim ((- H),X) = - (lim (H,X)) )

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) = |.(lim (H,X)).| & - H is_point_conv_on X & lim ((- H),X) = - (lim (H,X)) )

proof end;

theorem :: SEQFUNC:42

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

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 Th42: :: SEQFUNC:43

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

|.(((H . n) . x) - ((lim (H,X)) . x)).| < r ) ) )

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

|.(((H . n) . x) - ((lim (H,X)) . x)).| < r ) ) )

proof end;

theorem :: SEQFUNC:44

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) | X is continuous ) holds

(lim (H,X)) | X is continuous

for H being Functional_Sequence of REAL,REAL st H is_unif_conv_on X & ( for n being Nat holds (H . n) | X is continuous ) holds

(lim (H,X)) | X is continuous

proof end;