:: Functional Sequence from a Domain to a Domain
:: by Beata Perkowska
::
:: Received May 22, 1992
:: Copyright (c) 1992-2012 Association of Mizar Users


begin

definition
let D1, D2 be set ;
mode Functional_Sequence of D1,D2 is sequence of (PFuncs (D1,D2));
end;

definition
let D1, D2 be set ;
let F be Functional_Sequence of D1,D2;
let n be Nat;
:: original:.
redefine funcF . n ->  PartFunc of D1,D2;
coherence
 F . n is PartFunc of D1,D2
proofend;
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 ) ) )
proofend;

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 Element of NAT holds f . n is PartFunc of D1,D2 ) ) )
proofend;

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

definition
let D be non empty set ;
let H be Functional_Sequence of D,REAL;
let r be real number ;
funcr (#) H ->  Functional_Sequence of D,REAL means :Def1: :: SEQFUNC:def 1
 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)
proofend;
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
proofend;
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 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;
funcH "  ->  Functional_Sequence of D,REAL means :Def2: :: SEQFUNC:def 2
 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) ^
proofend;
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
proofend;
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)
proofend;
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
proofend;
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)
proofend;
func abs H ->  Functional_Sequence of D,REAL means :Def4: :: SEQFUNC:def 4
 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)
proofend;
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
proofend;
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)
proofend;
end;

:: deftheorem Def2 defines " SEQFUNC:def_2_:_
 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 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 abs SEQFUNC:def_4_:_
 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;
funcG + H ->  Functional_Sequence of D,REAL means :Def5: :: SEQFUNC:def 5
 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)
proofend;
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
proofend;
end;

:: deftheorem Def5 defines + SEQFUNC:def_5_:_
 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;
funcG - H ->  Functional_Sequence of D,REAL equals :: SEQFUNC:def 6
G + (- H);
correctness
coherence
G + (- H) is Functional_Sequence of D,REAL;
;
end;

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

definition
let D be non empty set ;
let G, H be Functional_Sequence of D,REAL;
funcG (#) H ->  Functional_Sequence of D,REAL means :Def7: :: SEQFUNC:def 7
 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)
proofend;
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
proofend;
end;

:: deftheorem Def7 defines (#) SEQFUNC:def_7_:_
 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;
funcG / H ->  Functional_Sequence of D,REAL equals :: SEQFUNC:def 8
G (#) (H ");
correctness
coherence
G (#) (H ") is Functional_Sequence of D,REAL;
;
end;

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

theorem :: SEQFUNC:2
for D being non empty set
for H1, G, H being Functional_Sequence of D,REAL holds
( H1 = G / H iff for n being Element of NAT holds H1 . n = (G . n) / (H . n) )
proofend;

theorem Th3: :: SEQFUNC:3
for D being non empty set
for H1, G, H being Functional_Sequence of D,REAL holds
( H1 = G - H iff for n being Element of NAT holds H1 . n = (G . n) - (H . n) )
proofend;

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

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

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

theorem :: SEQFUNC:7
for D being non empty set
for H being Functional_Sequence of D,REAL holds - H = (- 1) (#) H
proofend;

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

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

theorem :: SEQFUNC:10
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)
proofend;

theorem :: SEQFUNC:11
for D being non empty set
for H being Functional_Sequence of D,REAL holds 1 (#) H = H
proofend;

theorem :: SEQFUNC:12
canceled;

theorem :: SEQFUNC:13
for D being non empty set
for G, H being Functional_Sequence of D,REAL holds (G ") (#) (H ") = (G (#) H) "
proofend;

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

theorem Th15: :: SEQFUNC:15
for D being non empty set
for H being Functional_Sequence of D,REAL holds (abs H) " = abs (H ")
proofend;

theorem Th16: :: 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)
proofend;

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

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) = (abs r) (#) (abs H)
proofend;

definition
let D1, D2 be set ;
let F be Functional_Sequence of D1,D2;
let X be set ;
predX common_on_dom F means :Def9: :: SEQFUNC:def 9
( X <> {} &amp; ( for n being Element of NAT holds X c= dom (F . n) ) );
end;

:: deftheorem Def9 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 <> {} &amp; ( for n being Element of 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;
funcH # x ->  Real_Sequence means :Def10: :: SEQFUNC:def 10
 for n being Element of NAT holds it . n = (H . n) . x;
existence
 ex b1 being Real_Sequence st
for n being Element of NAT holds b1 . n = (H . n) . x
proofend;
uniqueness
 for b1, b2 being Real_Sequence st ( for n being Element of NAT holds b1 . n = (H . n) . x ) &amp; ( for n being Element of NAT holds b2 . n = (H . n) . x ) holds
b1 = b2
proofend;
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 b4 being Real_Sequence holds
( b4 = H # x iff for n being Element of 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 ;
predH is_point_conv_on X means :Def11: :: SEQFUNC:def 11
( X common_on_dom H &amp; ex f being PartFunc of D,REAL st
( X = dom f &amp; ( for x being Element of D st x in X holds
for p being Real st p > 0 holds
ex k being Element of NAT st
for n being Element of NAT st n >= k holds
abs (((H . n) . x) - (f . x)) < p ) ) );
end;

:: deftheorem Def11 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 &amp; ex f being PartFunc of D,REAL st
( X = dom f &amp; ( for x being Element of D st x in X holds
for p being Real st p > 0 holds
ex k being Element of NAT st
for n being Element of NAT st n >= k holds
abs (((H . n) . x) - (f . x)) < p ) ) ) );

theorem Th19: :: 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 &amp; ex f being PartFunc of D,REAL st
( X = dom f &amp; ( for x being Element of D st x in X holds
( H # x is convergent &amp; lim (H # x) = f . x ) ) ) ) )
proofend;

theorem Th20: :: 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 &amp; ( for x being Element of D st x in X holds
H # x is convergent ) ) )
proofend;

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

:: deftheorem Def12 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 &amp; ex f being PartFunc of D,REAL st
( X = dom f &amp; ( for p being Real st p > 0 holds
ex k being Element of NAT st
for n being Element of NAT
for x being Element of D st n >= k &amp; 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 :Def13: :: SEQFUNC:def 13
( dom it = X &amp; ( 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 &amp; ( for x being Element of D st x in dom b1 holds
b1 . x = lim (H # x) ) )
proofend;
uniqueness
 for b1, b2 being PartFunc of D,REAL st dom b1 = X &amp; ( for x being Element of D st x in dom b1 holds
b1 . x = lim (H # x) ) &amp; dom b2 = X &amp; ( for x being Element of D st x in dom b2 holds
b2 . x = lim (H # x) ) holds
b1 = b2
proofend;
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 b4 being PartFunc of D,REAL holds
( b4 = lim (H,X) iff ( dom b4 = X &amp; ( for x being Element of D st x in dom b4 holds
b4 . x = lim (H # x) ) ) );

theorem Th21: :: 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 &amp; ( for x being Element of D st x in X holds
for p being Real st p > 0 holds
ex k being Element of NAT st
for n being Element of NAT st n >= k holds
abs (((H . n) . x) - (f . x)) < p ) ) )
proofend;

theorem Th22: :: 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
proofend;

theorem Th23: :: SEQFUNC:23
for D being non empty set
for H being Functional_Sequence of D,REAL
for Y, X being set st Y c= X &amp; Y <> {} &amp; X common_on_dom H holds
Y common_on_dom H
proofend;

theorem :: SEQFUNC:24
for D being non empty set
for H being Functional_Sequence of D,REAL
for Y, X being set st Y c= X &amp; Y <> {} &amp; H is_point_conv_on X holds
( H is_point_conv_on Y &amp; (lim (H,X)) | Y = lim (H,Y) )
proofend;

theorem :: SEQFUNC:25
for D being non empty set
for H being Functional_Sequence of D,REAL
for Y, X being set st Y c= X &amp; Y <> {} &amp; H is_unif_conv_on X holds
H is_unif_conv_on Y
proofend;

theorem Th26: :: 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
proofend;

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

theorem Th28: :: 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 &amp; {x} common_on_dom H2 holds
( (H1 # x) + (H2 # x) = (H1 + H2) # x &amp; (H1 # x) - (H2 # x) = (H1 - H2) # x &amp; (H1 # x) (#) (H2 # x) = (H1 (#) H2) # x )
proofend;

theorem Th29: :: 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) &amp; (- H) # x = - (H # x) )
proofend;

theorem Th30: :: 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)
proofend;

theorem Th31: :: 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 &amp; X common_on_dom H2 holds
for x being Element of D st x in X holds
( (H1 # x) + (H2 # x) = (H1 + H2) # x &amp; (H1 # x) - (H2 # x) = (H1 - H2) # x &amp; (H1 # x) (#) (H2 # x) = (H1 (#) H2) # x )
proofend;

theorem Th32: :: SEQFUNC:32
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) &amp; (- H) # x = - (H # x) ) by Th29;

theorem Th33: :: 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)
proofend;

theorem Th34: :: 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 &amp; 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 &amp; (H1 # x) - (H2 # x) = (H1 - H2) # x &amp; (H1 # x) (#) (H2 # x) = (H1 (#) H2) # x )
proofend;

theorem :: SEQFUNC:35
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) &amp; (- H) # x = - (H # x) ) by Th32;

theorem :: SEQFUNC:36
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)
proofend;

theorem Th37: :: 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 &amp; X common_on_dom H2 holds
( X common_on_dom H1 + H2 &amp; X common_on_dom H1 - H2 &amp; X common_on_dom H1 (#) H2 )
proofend;

theorem Th38: :: 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 &amp; X common_on_dom - H )
proofend;

theorem Th39: :: 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
proofend;

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 &amp; H2 is_point_conv_on X holds
( H1 + H2 is_point_conv_on X &amp; lim ((H1 + H2),X) = (lim (H1,X)) + (lim (H2,X)) &amp; H1 - H2 is_point_conv_on X &amp; lim ((H1 - H2),X) = (lim (H1,X)) - (lim (H2,X)) &amp; H1 (#) H2 is_point_conv_on X &amp; lim ((H1 (#) H2),X) = (lim (H1,X)) (#) (lim (H2,X)) )
proofend;

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 &amp; lim ((abs H),X) = abs (lim (H,X)) &amp; - H is_point_conv_on X &amp; lim ((- H),X) = - (lim (H,X)) )
proofend;

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 &amp; lim ((r (#) H),X) = r (#) (lim (H,X)) )
proofend;

theorem Th43: :: 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 &amp; H is_point_conv_on X &amp; ( for r being Real st 0 < r holds
ex k being Element of NAT st
for n being Element of NAT
for x being Element of D st n >= k &amp; x in X holds
abs (((H . n) . x) - ((lim (H,X)) . x)) < r ) ) )
proofend;

theorem :: SEQFUNC:44
for X being set
for H being Functional_Sequence of REAL,REAL st H is_unif_conv_on X &amp; ( for n being Element of NAT holds (H . n) | X is continuous ) holds
(lim (H,X)) | X is continuous
proofend;