seqfunc.miz

begin

 reserve D for non empty set,

D1,D2,x,y for set,

n,k for Nat,

p,x1,r for Real,

f for Function;

 definition

 let D1, D2;

 mode Functional_Sequence of D1,D2 is sequence of ( PFuncs (D1,D2));

 end

 reserve F for Functional_Sequence of D1, D2;

 definition

 let D1, D2, F;

 let n be natural Number;

 :: original: .

 redefine

 func F . n -> PartFunc of D1, D2 ;

 coherence

 proof

 n in NAT by ORDINAL1:def 12;

 then n in ( dom F) by FUNCT_2:def 1;

 then (F . n) in ( rng F) by FUNCT_1:def 3;

 hence thesis by PARTFUN1: 46;

 end;

 end

 reserve G,H,H1,H2,J for Functional_Sequence of D, REAL ;



 Lm1: f is Functional_Sequence of D1, D2 iff (( dom f) = NAT & for x st x in NAT holds (f . x) is PartFunc of D1, D2)

 proof

 thus f is Functional_Sequence of D1, D2 implies (( dom f) = NAT & for x st x in NAT holds (f . x) is PartFunc of D1, D2)

 proof

 assume

 A1: f is Functional_Sequence of D1, D2;

 hence ( dom f) = NAT by FUNCT_2:def 1;

 let x;

 assume x in NAT ;

 then x in ( dom f) by A1, FUNCT_2:def 1;

 then

 A2: (f . x) in ( rng f) by FUNCT_1:def 3;

 ( rng f) c= ( PFuncs (D1,D2)) by A1, RELAT_1:def 19;

 hence thesis by A2, PARTFUN1: 46;

 end;

 assume that

 A3: ( dom f) = NAT and

 A4: for x st x in NAT holds (f . x) is PartFunc of D1, D2;

 now

 let y be object;

 assume y in ( rng f);

 then

 consider x be object such that

 A5: x in ( dom f) and

 A6: y = (f . x) by FUNCT_1:def 3;

 (f . x) is PartFunc of D1, D2 by A3, A4, A5;

 hence y in ( PFuncs (D1,D2)) by A6, PARTFUN1: 45;

 end;

 then ( rng f) c= ( PFuncs (D1,D2));

 hence thesis by A3, FUNCT_2:def 1, RELSET_1: 4;

 end;

 theorem :: SEQFUNC:1

 f is Functional_Sequence of D1, D2 iff ( dom f) = NAT & for n holds (f . n) is PartFunc of D1, D2

 proof

 thus f is Functional_Sequence of D1, D2 implies ( dom f) = NAT & for n holds (f . n) is PartFunc of D1, D2 by Lm1, ORDINAL1:def 12;

 assume that

 A1: ( dom f) = NAT and

 A2: for n holds (f . n) is PartFunc of D1, D2;

 for x holds x in NAT implies (f . x) is PartFunc of D1, D2 by A2;

 hence thesis by A1, Lm1;

 end;

 scheme :: SEQFUNC:sch1

 ExFuncSeq { D1() -> set , D2() -> set , F( object) -> PartFunc of D1(), D2() } :

ex G be Functional_Sequence of D1(), D2() st for n be Nat holds (G . n) = F(n);

 defpred P[ object, object] means $2 = F($1);



 A1: for x be object st x in NAT holds ex y be object st P[x, y];

 consider f such that

 A2: ( dom f) = NAT and

 A3: for x be object st x in NAT holds P[x, (f . x)] from CLASSES1:sch 1( A1);

 now

 let x;

 assume x in NAT ;

 then (f . x) = F(x) by A3;

 hence (f . x) is PartFunc of D1(), D2();

 end;

 then

 reconsider f as Functional_Sequence of D1(), D2() by A2, Lm1;

 take f;

 let n be Nat;

 n in NAT by ORDINAL1:def 12;

 hence thesis by A3;

 end;

 definition

 let D, H;

 let r be Real;

 :: SEQFUNC:def1

 func r (#) H -> Functional_Sequence of D, REAL means

 : Def1: for n be Nat holds (it . n) = (r (#) (H . n));

 existence

 proof

 deffunc U( Nat) = (r (#) (H . $1));

 thus ex f be Functional_Sequence of D, REAL st for n be Nat holds (f . n) = U(n) from ExFuncSeq;

 end;

 uniqueness

 proof

 let H1, H2 such that

 A1: for n be Nat holds (H1 . n) = (r (#) (H . n)) and

 A2: for n be Nat holds (H2 . n) = (r (#) (H . n));

 now

 let n be Element of NAT ;

 (H1 . n) = (r (#) (H . n)) by A1;

 hence (H1 . n) = (H2 . n) by A2;

 end;

 hence H1 = H2 by FUNCT_2: 63;

 end;

 end

 definition

 let D, H;

 :: SEQFUNC:def2

 func H " -> Functional_Sequence of D, REAL means

 : Def2: for n be Nat holds (it . n) = ((H . n) ^ );

 existence

 proof

 deffunc U( Nat) = ((H . $1) ^ );

 thus ex f be Functional_Sequence of D, REAL st for n be Nat holds (f . n) = U(n) from ExFuncSeq;

 end;

 uniqueness

 proof

 let H1, H2 such that

 A1: for n be Nat holds (H1 . n) = ((H . n) ^ ) and

 A2: for n be Nat holds (H2 . n) = ((H . n) ^ );

 now

 let n be Element of NAT ;

 (H1 . n) = ((H . n) ^ ) by A1;

 hence (H1 . n) = (H2 . n) by A2;

 end;

 hence H1 = H2 by FUNCT_2: 63;

 end;

 :: SEQFUNC:def3

 func - H -> Functional_Sequence of D, REAL means

 : Def3: for n be Nat holds (it . n) = ( - (H . n));

 existence

 proof

 take (( - 1) (#) H);

 let n be Nat;

 thus thesis by Def1;

 end;

 uniqueness

 proof

 let H1, H2 such that

 A3: for n be Nat holds (H1 . n) = ( - (H . n)) and

 A4: for n be Nat holds (H2 . n) = ( - (H . n));

 now

 let n be Element of NAT ;

 (H1 . n) = ( - (H . n)) by A3;

 hence (H1 . n) = (H2 . n) by A4;

 end;

 hence H1 = H2 by FUNCT_2: 63;

 end;

 involutiveness

 proof

 let G,H be Functional_Sequence of D, REAL such that

 A5: for n be Nat holds (G . n) = ( - (H . n));

 let n be Nat;



 thus (H . n) = ( - ( - (H . n)))

 .= ( - (G . n)) by A5;

 end;

 :: SEQFUNC:def4

 func abs (H) -> Functional_Sequence of D, REAL means

 : Def4: for n be Nat holds (it . n) = ( abs (H . n));

 existence

 proof

 deffunc U( Nat) = ( abs (H . $1));

 thus ex f be Functional_Sequence of D, REAL st for n be Nat holds (f . n) = U(n) from ExFuncSeq;

 end;

 uniqueness

 proof

 let H1, H2 such that

 A6: for n be Nat holds (H1 . n) = ( abs (H . n)) and

 A7: for n be Nat holds (H2 . n) = ( abs (H . n));

 now

 let n be Element of NAT ;

 (H2 . n) = ( abs (H . n)) by A7;

 hence (H1 . n) = (H2 . n) by A6;

 end;

 hence H1 = H2 by FUNCT_2: 63;

 end;

 projectivity

 proof

 let G,H be Functional_Sequence of D, REAL such that

 A8: for n be Nat holds (G . n) = ( abs (H . n));

 let n be Nat;



 thus (G . n) = ( abs ( abs (H . n))) by A8

 .= ( abs (G . n)) by A8;

 end;

 end

 definition

 let D, G, H;

 :: SEQFUNC:def5

 func G + H -> Functional_Sequence of D, REAL means

 : Def5: for n be Nat holds (it . n) = ((G . n) + (H . n));

 existence

 proof

 deffunc U( Nat) = ((G . $1) + (H . $1));

 thus ex f be Functional_Sequence of D, REAL st for n be Nat holds (f . n) = U(n) from ExFuncSeq;

 end;

 uniqueness

 proof

 let H1, H2 such that

 A1: for n be Nat holds (H1 . n) = ((G . n) + (H . n)) and

 A2: for n be Nat holds (H2 . n) = ((G . n) + (H . n));

 now

 let n be Element of NAT ;

 (H1 . n) = ((G . n) + (H . n)) by A1;

 hence (H1 . n) = (H2 . n) by A2;

 end;

 hence H1 = H2 by FUNCT_2: 63;

 end;

 end

 definition

 let D, G, H;

 :: SEQFUNC:def6

 func G - H -> Functional_Sequence of D, REAL equals (G + ( - H));

 correctness ;

 end

 definition

 let D, G, H;

 :: SEQFUNC:def7

 func G (#) H -> Functional_Sequence of D, REAL means

 : Def7: for n be Nat holds (it . n) = ((G . n) (#) (H . n));

 existence

 proof

 deffunc U( Nat) = ((G . $1) (#) (H . $1));

 thus ex f be Functional_Sequence of D, REAL st for n be Nat holds (f . n) = U(n) from ExFuncSeq;

 end;

 uniqueness

 proof

 let H1, H2 such that

 A1: for n be Nat holds (H1 . n) = ((G . n) (#) (H . n)) and

 A2: for n be Nat holds (H2 . n) = ((G . n) (#) (H . n));

 now

 let n be Element of NAT ;

 (H1 . n) = ((G . n) (#) (H . n)) by A1;

 hence (H1 . n) = (H2 . n) by A2;

 end;

 hence H1 = H2 by FUNCT_2: 63;

 end;

 end

 definition

 let D, H, G;

 :: SEQFUNC:def8

 func G / H -> Functional_Sequence of D, REAL equals (G (#) (H " ));

 correctness ;

 end

 theorem :: SEQFUNC:2

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

 proof

 thus H1 = (G / H) implies for n holds (H1 . n) = ((G . n) / (H . n))

 proof

 assume

 A1: H1 = (G / H);

 let n;



 thus (H1 . n) = ((G . n) (#) ((H " ) . n)) by A1, Def7

 .= ((G . n) (#) ((H . n) ^ )) by Def2

 .= ((G . n) / (H . n)) by RFUNCT_1: 31;

 end;

 assume

 A2: for n holds (H1 . n) = ((G . n) / (H . n));

 now

 let n be Element of NAT ;



 thus (H1 . n) = ((G . n) / (H . n)) by A2

 .= ((G . n) (#) ((H . n) ^ )) by RFUNCT_1: 31

 .= ((G . n) (#) ((H " ) . n)) by Def2

 .= ((G / H) . n) by Def7;

 end;

 hence thesis by FUNCT_2: 63;

 end;

 theorem :: SEQFUNC:3



 Th3: H1 = (G - H) iff for n holds (H1 . n) = ((G . n) - (H . n))

 proof

 thus H1 = (G - H) implies for n holds (H1 . n) = ((G . n) - (H . n))

 proof

 assume

 A1: H1 = (G - H);

 let n;



 thus (H1 . n) = ((G . n) + (( - H) . n)) by A1, Def5

 .= ((G . n) - (H . n)) by Def3;

 end;

 assume

 A2: for n holds (H1 . n) = ((G . n) - (H . n));

 now

 let n be Element of NAT ;



 thus (H1 . n) = ((G . n) - (H . n)) by A2

 .= ((G . n) + (( - H) . n)) by Def3

 .= ((G - H) . n) by Def5;

 end;

 hence thesis by FUNCT_2: 63;

 end;

 theorem :: SEQFUNC:4

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

 proof

 now

 let n be Element of NAT ;



 thus ((G + H) . n) = ((H . n) + (G . n)) by Def5

 .= ((H + G) . n) by Def5;

 end;

 hence (G + H) = (H + G) by FUNCT_2: 63;

 now

 let n be Element of NAT ;



 thus (((G + H) + J) . n) = (((G + H) . n) + (J . n)) by Def5

 .= (((G . n) + (H . n)) + (J . n)) by Def5

 .= ((G . n) + ((H . n) + (J . n))) by RFUNCT_1: 8

 .= ((G . n) + ((H + J) . n)) by Def5

 .= ((G + (H + J)) . n) by Def5;

 end;

 hence thesis by FUNCT_2: 63;

 end;

 theorem :: SEQFUNC:5



 Th5: (G (#) H) = (H (#) G) & ((G (#) H) (#) J) = (G (#) (H (#) J))

 proof

 now

 let n be Element of NAT ;



 thus ((G (#) H) . n) = ((H . n) (#) (G . n)) by Def7

 .= ((H (#) G) . n) by Def7;

 end;

 hence (G (#) H) = (H (#) G) by FUNCT_2: 63;

 now

 let n be Element of NAT ;



 thus (((G (#) H) (#) J) . n) = (((G (#) H) . n) (#) (J . n)) by Def7

 .= (((G . n) (#) (H . n)) (#) (J . n)) by Def7

 .= ((G . n) (#) ((H . n) (#) (J . n))) by RFUNCT_1: 9

 .= ((G . n) (#) ((H (#) J) . n)) by Def7

 .= ((G (#) (H (#) J)) . n) by Def7;

 end;

 hence thesis by FUNCT_2: 63;

 end;

 theorem :: SEQFUNC:6

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

 proof

 now

 let n be Element of NAT ;



 thus (((G + H) (#) J) . n) = (((G + H) . n) (#) (J . n)) by Def7

 .= (((G . n) + (H . n)) (#) (J . n)) by Def5

 .= (((G . n) (#) (J . n)) + ((H . n) (#) (J . n))) by RFUNCT_1: 10

 .= (((G (#) J) . n) + ((H . n) (#) (J . n))) by Def7

 .= (((G (#) J) . n) + ((H (#) J) . n)) by Def7

 .= (((G (#) J) + (H (#) J)) . n) by Def5;

 end;

 hence ((G + H) (#) J) = ((G (#) J) + (H (#) J)) by FUNCT_2: 63;



 hence (J (#) (G + H)) = ((G (#) J) + (H (#) J)) by Th5

 .= ((J (#) G) + (H (#) J)) by Th5

 .= ((J (#) G) + (J (#) H)) by Th5;

 end;

 theorem :: SEQFUNC:7

 ( - H) = (( - 1) (#) H)

 proof

 now

 let n be Element of NAT ;



 thus (( - H) . n) = ( - (H . n)) by Def3

 .= ((( - 1) (#) H) . n) by Def1;

 end;

 hence thesis by FUNCT_2: 63;

 end;

 theorem :: SEQFUNC:8

 ((G - H) (#) J) = ((G (#) J) - (H (#) J)) & ((J (#) G) - (J (#) H)) = (J (#) (G - H))

 proof

 now

 let n be Element of NAT ;



 thus (((G - H) (#) J) . n) = (((G - H) . n) (#) (J . n)) by Def7

 .= (((G . n) - (H . n)) (#) (J . n)) by Th3

 .= (((G . n) (#) (J . n)) - ((H . n) (#) (J . n))) by RFUNCT_1: 14

 .= (((G (#) J) . n) - ((H . n) (#) (J . n))) by Def7

 .= (((G (#) J) . n) - ((H (#) J) . n)) by Def7

 .= (((G (#) J) - (H (#) J)) . n) by Th3;

 end;

 hence

 A1: ((G - H) (#) J) = ((G (#) J) - (H (#) J)) by FUNCT_2: 63;



 thus ((J (#) G) - (J (#) H)) = ((J (#) G) - (H (#) J)) by Th5

 .= ((G - H) (#) J) by A1, Th5

 .= (J (#) (G - H)) by Th5;

 end;

 theorem :: SEQFUNC:9

 (r (#) (G + H)) = ((r (#) G) + (r (#) H)) & (r (#) (G - H)) = ((r (#) G) - (r (#) H))

 proof

 now

 let n be Element of NAT ;



 thus ((r (#) (G + H)) . n) = (r (#) ((G + H) . n)) by Def1

 .= (r (#) ((G . n) + (H . n))) by Def5

 .= ((r (#) (G . n)) + (r (#) (H . n))) by RFUNCT_1: 16

 .= (((r (#) G) . n) + (r (#) (H . n))) by Def1

 .= (((r (#) G) . n) + ((r (#) H) . n)) by Def1

 .= (((r (#) G) + (r (#) H)) . n) by Def5;

 end;

 hence (r (#) (G + H)) = ((r (#) G) + (r (#) H)) by FUNCT_2: 63;

 now

 let n be Element of NAT ;



 thus ((r (#) (G - H)) . n) = (r (#) ((G - H) . n)) by Def1

 .= (r (#) ((G . n) - (H . n))) by Th3

 .= ((r (#) (G . n)) - (r (#) (H . n))) by RFUNCT_1: 18

 .= (((r (#) G) . n) - (r (#) (H . n))) by Def1

 .= (((r (#) G) . n) - ((r (#) H) . n)) by Def1

 .= (((r (#) G) - (r (#) H)) . n) by Th3;

 end;

 hence thesis by FUNCT_2: 63;

 end;

 theorem :: SEQFUNC:10

 ((r * p) (#) H) = (r (#) (p (#) H))

 proof

 now

 let n be Element of NAT ;



 thus (((r * p) (#) H) . n) = ((r * p) (#) (H . n)) by Def1

 .= (r (#) (p (#) (H . n))) by RFUNCT_1: 17

 .= (r (#) ((p (#) H) . n)) by Def1

 .= ((r (#) (p (#) H)) . n) by Def1;

 end;

 hence thesis by FUNCT_2: 63;

 end;

 theorem :: SEQFUNC:11

 (1 (#) H) = H

 proof

 now

 let n be Element of NAT ;



 thus ((1 (#) H) . n) = (1 (#) (H . n)) by Def1

 .= (H . n) by RFUNCT_1: 21;

 end;

 hence thesis by FUNCT_2: 63;

 end;

 ::$Canceled

 theorem :: SEQFUNC:13

 ((G " ) (#) (H " )) = ((G (#) H) " )

 proof

 now

 let n be Element of NAT ;



 thus (((G " ) (#) (H " )) . n) = (((G " ) . n) (#) ((H " ) . n)) by Def7

 .= (((G . n) ^ ) (#) ((H " ) . n)) by Def2

 .= (((G . n) ^ ) (#) ((H . n) ^ )) by Def2

 .= (((G . n) (#) (H . n)) ^ ) by RFUNCT_1: 27

 .= (((G (#) H) . n) ^ ) by Def7

 .= (((G (#) H) " ) . n) by Def2;

 end;

 hence thesis by FUNCT_2: 63;

 end;

 theorem :: SEQFUNC:14

 r <> 0 implies ((r (#) H) " ) = ((r " ) (#) (H " ))

 proof

 assume

 A1: r <> 0 ;

 now

 let n be Element of NAT ;



 thus (((r (#) H) " ) . n) = (((r (#) H) . n) ^ ) by Def2

 .= ((r (#) (H . n)) ^ ) by Def1

 .= ((r " ) (#) ((H . n) ^ )) by A1, RFUNCT_1: 28

 .= ((r " ) (#) ((H " ) . n)) by Def2

 .= (((r " ) (#) (H " )) . n) by Def1;

 end;

 hence thesis by FUNCT_2: 63;

 end;

 theorem :: SEQFUNC:15



 Th14: (( abs H) " ) = ( abs (H " ))

 proof

 now

 let n be Element of NAT ;



 thus (( abs (H " )) . n) = ( abs ((H " ) . n)) by Def4

 .= ( abs ((H . n) ^ )) by Def2

 .= (( abs (H . n)) ^ ) by RFUNCT_1: 30

 .= ((( abs H) . n) ^ ) by Def4

 .= ((( abs H) " ) . n) by Def2;

 end;

 hence thesis by FUNCT_2: 63;

 end;

 theorem :: SEQFUNC:16



 Th15: ( abs (G (#) H)) = (( abs G) (#) ( abs H))

 proof

 now

 let n be Element of NAT ;



 thus (( abs (G (#) H)) . n) = ( abs ((G (#) H) . n)) by Def4

 .= ( abs ((G . n) (#) (H . n))) by Def7

 .= (( abs (G . n)) (#) ( abs (H . n))) by RFUNCT_1: 24

 .= ((( abs G) . n) (#) ( abs (H . n))) by Def4

 .= ((( abs G) . n) (#) (( abs H) . n)) by Def4

 .= ((( abs G) (#) ( abs H)) . n) by Def7;

 end;

 hence thesis by FUNCT_2: 63;

 end;

 theorem :: SEQFUNC:17

 ( abs (G / H)) = (( abs G) / ( abs H))

 proof



 thus ( abs (G / H)) = (( abs G) (#) ( abs (H " ))) by Th15

 .= (( abs G) / ( abs H)) by Th14;

 end;

 theorem :: SEQFUNC:18

 ( abs (r (#) H)) = ( |.r.| (#) ( abs H))

 proof

 now

 let n be Element of NAT ;



 thus (( abs (r (#) H)) . n) = ( abs ((r (#) H) . n)) by Def4

 .= ( abs (r (#) (H . n))) by Def1

 .= ( |.r.| (#) ( abs (H . n))) by RFUNCT_1: 25

 .= ( |.r.| (#) (( abs H) . n)) by Def4

 .= (( |.r.| (#) ( abs H)) . n) by Def1;

 end;

 hence thesis by FUNCT_2: 63;

 end;

 reserve x for Element of D,

X,Y for set,

S1,S2 for Real_Sequence,

f for PartFunc of D, REAL ;

 definition

 let D1, D2, F, X;

 :: SEQFUNC:def9

 pred X common_on_dom F means X <> {} & for n holds X c= ( dom (F . n));

 end

 definition

 let D, H, x;

 :: SEQFUNC:def10

 func H # x -> Real_Sequence means

 : Def10: for n holds (it . n) = ((H . n) . x);

 existence

 proof

 deffunc U( Nat) = ((H . $1) . x);

 consider f be Real_Sequence such that

 A1: for n be Nat holds (f . n) = U(n) from SEQ_1:sch 1;

 take f;

 thus thesis by A1;

 end;

 uniqueness

 proof

 let S1, S2 such that

 A2: for n holds (S1 . n) = ((H . n) . x) and

 A3: for n holds (S2 . n) = ((H . n) . x);

 now

 let n be Element of NAT ;

 (S1 . n) = ((H . n) . x) by A2;

 hence (S1 . n) = (S2 . n) by A3;

 end;

 hence thesis by FUNCT_2: 63;

 end;

 end

 definition

 let D, H, X;

 :: SEQFUNC:def11

 pred H is_point_conv_on X means X common_on_dom H & ex f st X = ( dom f) & for x st x in X holds for p st p > 0 holds ex k st for n st n >= k holds |.(((H . n) . x) - (f . x)).| < p;

 end

 theorem :: SEQFUNC:19



 Th18: H is_point_conv_on X iff X common_on_dom H & ex f st X = ( dom f) & for x st x in X holds (H # x) is convergent & ( lim (H # x)) = (f . x)

 proof

 thus H is_point_conv_on X implies X common_on_dom H & ex f st X = ( dom f) & for x st x in X holds (H # x) is convergent & ( lim (H # x)) = (f . x)

 proof

 assume

 A1: H is_point_conv_on X;

 hence X common_on_dom H;

 consider f such that

 A2: X = ( dom f) and

 A3: for x st x in X holds for p st p > 0 holds ex k st for n st n >= k holds |.(((H . n) . x) - (f . x)).| 0 ;

 consider k such that

 A7: for n st n >= k holds |.(((H . n) . x) - (f . x)).| = k;

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

 hence |.(((H # x) . n) - (f . x)).| < p by Def10;

 end;

 hence (H # x) is convergent by SEQ_2:def 6;

 hence thesis by A5, SEQ_2:def 7;

 end;

 assume

 A8: X common_on_dom H;

 given f such that

 A9: X = ( dom f) and

 A10: for x st x in X holds (H # x) is convergent & ( lim (H # x)) = (f . x);

 ex f st X = ( dom f) & for x st x in X holds for p st p > 0 holds ex k st for n st n >= k holds |.(((H . n) . x) - (f . x)).| < p

 proof

 take f;

 thus X = ( dom f) by A9;

 let x;

 assume x in X;

 then

 A11: (H # x) is convergent & ( lim (H # x)) = (f . x) by A10;

 let p;

 assume p > 0 ;

 then

 consider k be Nat such that

 A12: for n be Nat st n >= k holds |.(((H # x) . n) - (f . x)).| = k;

 then |.(((H # x) . n) - (f . x)).| < p by A12;

 hence thesis by Def10;

 end;

 hence thesis by A8;

 end;

 theorem :: SEQFUNC:20



 Th19: H is_point_conv_on X iff X common_on_dom H & for x st x in X holds (H # x) is convergent

 proof

 defpred X[ set] means $1 in X;

 deffunc U( Element of D) = ( In (( lim (H # $1)), REAL ));

 consider f such that

 A1: for x holds x in ( dom f) iff X[x] and

 A2: for x st x in ( dom f) holds (f . x) = U(x) from SEQ_1:sch 3;

 thus H is_point_conv_on X implies X common_on_dom H & for x st x in X holds (H # x) is convergent

 proof

 assume

 A3: H is_point_conv_on X;

 hence X common_on_dom H;

 let x;

 assume

 A4: x in X;

 ex f st X = ( dom f) & for x st x in X holds (H # x) is convergent & ( lim (H # x)) = (f . x) by A3, Th18;

 hence thesis by A4;

 end;

 assume that

 A5: X common_on_dom H and

 A6: for x st x in X holds (H # x) is convergent;

 now

 take f;

 thus

 A7: X = ( dom f)

 proof

 thus X c= ( dom f)

 proof

 let x be object such that

 A8: x in X;

 X c= ( dom (H . 0 )) by A5;

 then X c= D by XBOOLE_1: 1;

 then

 reconsider x9 = x as Element of D by A8;

 x9 in ( dom f) by A1, A8;

 hence thesis;

 end;

 let x be object;

 assume x in ( dom f);

 hence thesis by A1;

 end;

 let x;

 assume

 A9: x in X;

 hence (H # x) is convergent by A6;



 thus (f . x) = U(x) by A2, A7, A9

 .= ( lim (H # x));

 end;

 hence thesis by A5, Th18;

 end;

 definition

 let D, H, X;

 :: SEQFUNC:def12

 pred H is_unif_conv_on X means X common_on_dom H & ex f st X = ( dom f) & for p st p > 0 holds ex k st for n, x st n >= k & x in X holds |.(((H . n) . x) - (f . x)).| < p;

 end

 definition

 let D, H, X;

 assume

 A1: H is_point_conv_on X;

 :: SEQFUNC:def13

 func lim (H,X) -> PartFunc of D, REAL means

 : Def13: ( dom it ) = X & for x st x in ( dom it ) holds (it . x) = ( lim (H # x));

 existence

 proof

 consider f such that

 A2: X = ( dom f) and

 A3: for x st x in X holds (H # x) is convergent & ( lim (H # x)) = (f . x) by A1, Th18;

 take f;

 thus ( dom f) = X by A2;

 let x;

 assume x in ( dom f);

 hence thesis by A2, A3;

 end;

 uniqueness

 proof

 deffunc U( Element of D) = ( lim (H # $1));

 thus for f1,f2 be PartFunc of D, REAL st ( dom f1) = X & (for x st x in ( dom f1) holds (f1 . x) = U(x)) & ( dom f2) = X & for x st x in ( dom f2) holds (f2 . x) = U(x) holds f1 = f2 from SEQ_1:sch 4;

 end;

 end

 theorem :: SEQFUNC:21



 Th20: H is_point_conv_on X implies (f = ( lim (H,X)) iff ( dom f) = X & for x st x in X holds for p st p > 0 holds ex k st for n st n >= k holds |.(((H . n) . x) - (f . x)).| < p)

 proof

 assume

 A1: H is_point_conv_on X;

 thus f = ( lim (H,X)) implies ( dom f) = X & for x st x in X holds for p st p > 0 holds ex k st for n st n >= k holds |.(((H . n) . x) - (f . x)).| < p

 proof

 assume

 A2: f = ( lim (H,X));

 hence

 A3: ( dom f) = X by A1, Def13;

 let x;

 assume

 A4: x in X;

 then

 A5: (H # x) is convergent by A1, Th19;

 let p;

 assume

 A6: p > 0 ;

 (f . x) = ( lim (H # x)) by A1, A2, A3, A4, Def13;

 then

 consider k be Nat such that

 A7: for n be Nat st n >= k holds |.(((H # x) . n) - (f . x)).| = k;

 then |.(((H # x) . n) - (f . x)).| 0 holds ex k st for n st n >= k holds |.(((H . n) . x) - (f . x)).| < p;

 now

 let x such that

 A10: x in ( dom f);

 A11:

 now

 let p be Real;

 assume

 A12: p > 0 ;

 consider k such that

 A13: for n st n >= k holds |.(((H . n) . x) - (f . x)).| = k;

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

 hence |.(((H # x) . n) - (f . x)).| < p by Def10;

 end;

 then (H # x) is convergent by SEQ_2:def 6;

 hence (f . x) = ( lim (H # x)) by A11, SEQ_2:def 7;

 end;

 hence thesis by A1, A8, Def13;

 end;

 theorem :: SEQFUNC:22



 Th21: H is_unif_conv_on X implies H is_point_conv_on X

 proof

 assume

 A1: H is_unif_conv_on X;

 A2:

 now

 consider f such that

 A3: X = ( dom f) and

 A4: for p st p > 0 holds ex k st for n, x st n >= k & x in X holds |.(((H . n) . x) - (f . x)).| 0 ;

 then

 consider k such that

 A6: for n, x st n >= k & x in X holds |.(((H . n) . x) - (f . x)).| = k;

 hence |.(((H . n) . x) - (f . x)).| {} & X common_on_dom H implies Y common_on_dom H

 proof

 assume that

 A1: Y c= X and

 A2: Y <> {} and

 A3: X common_on_dom H;

 now

 let n;

 X c= ( dom (H . n)) by A3;

 hence Y c= ( dom (H . n)) by A1;

 end;

 hence thesis by A2;

 end;

 theorem :: SEQFUNC:24

 Y c= X & Y <> {} & H is_point_conv_on X implies H is_point_conv_on Y & (( lim (H,X)) | Y) = ( lim (H,Y))

 proof

 assume that

 A1: Y c= X and

 A2: Y <> {} and

 A3: H is_point_conv_on X;

 consider f such that

 A4: X = ( dom f) and

 A5: for x st x in X holds for p st p > 0 holds ex k st for n st n >= k holds |.(((H . n) . x) - (f . x)).| < p by A3;

 A6:

 now

 take g = (f | Y);

 thus

 A7: Y = ( dom g) by A1, A4, RELAT_1: 62;

 let x;

 assume

 A8: x in Y;

 let p;

 assume p > 0 ;

 then

 consider k such that

 A9: for n st n >= k holds |.(((H . n) . x) - (f . x)).| = k;

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

 hence |.(((H . n) . x) - (g . x)).| < p by A7, A8, FUNCT_1: 47;

 end;

 X common_on_dom H by A3;

 then Y common_on_dom H by A1, A2, Th22;

 hence

 A10: H is_point_conv_on Y by A6;

 A11:

 now

 let x;

 assume

 A12: x in ( dom (( lim (H,X)) | Y));

 then

 A13: x in (( dom ( lim (H,X))) /\ Y) by RELAT_1: 61;

 then

 A14: x in ( dom ( lim (H,X))) by XBOOLE_0:def 4;

 x in Y by A13, XBOOLE_0:def 4;

 then

 A15: x in ( dom ( lim (H,Y))) by A10, Def13;



 thus ((( lim (H,X)) | Y) . x) = (( lim (H,X)) . x) by A12, FUNCT_1: 47

 .= ( lim (H # x)) by A3, A14, Def13

 .= (( lim (H,Y)) . x) by A10, A15, Def13;

 end;

 ( dom ( lim (H,X))) = X by A3, Def13;

 then (( dom ( lim (H,X))) /\ Y) = Y by A1, XBOOLE_1: 28;

 then ( dom (( lim (H,X)) | Y)) = Y by RELAT_1: 61;

 then ( dom (( lim (H,X)) | Y)) = ( dom ( lim (H,Y))) by A10, Def13;

 hence thesis by A11, PARTFUN1: 5;

 end;

 theorem :: SEQFUNC:25

 Y c= X & Y <> {} & H is_unif_conv_on X implies H is_unif_conv_on Y

 proof

 assume that

 A1: Y c= X and

 A2: Y <> {} and

 A3: H is_unif_conv_on X;

 consider f such that

 A4: ( dom f) = X and

 A5: for p st p > 0 holds ex k st for n, x st n >= k & x in X holds |.(((H . n) . x) - (f . x)).| < p by A3;

 A6:

 now

 take g = (f | Y);



 thus

 A7: ( dom g) = (( dom f) /\ Y) by RELAT_1: 61

 .= Y by A1, A4, XBOOLE_1: 28;

 let p;

 assume p > 0 ;

 then

 consider k such that

 A8: for n, x st n >= k & x in X holds |.(((H . n) . x) - (f . x)).| = k and

 A10: x in Y;

 |.(((H . n) . x) - (f . x)).| < p by A1, A8, A9, A10;

 hence |.(((H . n) . x) - (g . x)).| < p by A7, A10, FUNCT_1: 47;

 end;

 X common_on_dom H by A3;

 then Y common_on_dom H by A1, A2, Th22;

 hence thesis by A6;

 end;

 theorem :: SEQFUNC:26



 Th25: X common_on_dom H implies for x st x in X holds {x} common_on_dom H

 proof

 assume

 A1: X common_on_dom H;

 let x;

 assume

 A2: x in X;

 thus {x} <> {} ;

 now

 let n;

 X c= ( dom (H . n)) by A1;

 hence {x} c= ( dom (H . n)) by A2, ZFMISC_1: 31;

 end;

 hence thesis;

 end;

 theorem :: SEQFUNC:27

 H is_point_conv_on X implies for x st x in X holds {x} common_on_dom H by Th25;

 theorem :: SEQFUNC:28



 Th27: {x} common_on_dom H1 & {x} common_on_dom H2 implies ((H1 # x) + (H2 # x)) = ((H1 + H2) # x) & ((H1 # x) - (H2 # x)) = ((H1 - H2) # x) & ((H1 # x) (#) (H2 # x)) = ((H1 (#) H2) # x)

 proof

 assume that

 A1: {x} common_on_dom H1 and

 A2: {x} common_on_dom H2;

 now

 let n be Element of NAT ;



 A3: {x} c= ( dom (H2 . n)) by A2;

 x in {x} & {x} c= ( dom (H1 . n)) by A1, TARSKI:def 1;

 then x in (( dom (H1 . n)) /\ ( dom (H2 . n))) by A3, XBOOLE_0:def 4;

 then

 A4: x in ( dom ((H1 . n) + (H2 . n))) by VALUED_1:def 1;



 thus (((H1 # x) + (H2 # x)) . n) = (((H1 # x) . n) + ((H2 # x) . n)) by SEQ_1: 7

 .= (((H1 . n) . x) + ((H2 # x) . n)) by Def10

 .= (((H1 . n) . x) + ((H2 . n) . x)) by Def10

 .= (((H1 . n) + (H2 . n)) . x) by A4, VALUED_1:def 1

 .= (((H1 + H2) . n) . x) by Def5

 .= (((H1 + H2) # x) . n) by Def10;

 end;

 hence ((H1 # x) + (H2 # x)) = ((H1 + H2) # x) by FUNCT_2: 63;

 now

 let n be Element of NAT ;



 A5: {x} c= ( dom (H2 . n)) by A2;

 x in {x} & {x} c= ( dom (H1 . n)) by A1, TARSKI:def 1;

 then x in (( dom (H1 . n)) /\ ( dom (H2 . n))) by A5, XBOOLE_0:def 4;

 then

 A6: x in ( dom ((H1 . n) - (H2 . n))) by VALUED_1: 12;



 thus (((H1 # x) - (H2 # x)) . n) = (((H1 # x) . n) - ((H2 # x) . n)) by RFUNCT_2: 1

 .= (((H1 . n) . x) - ((H2 # x) . n)) by Def10

 .= (((H1 . n) . x) - ((H2 . n) . x)) by Def10

 .= (((H1 . n) - (H2 . n)) . x) by A6, VALUED_1: 13

 .= (((H1 - H2) . n) . x) by Th3

 .= (((H1 - H2) # x) . n) by Def10;

 end;

 hence ((H1 # x) - (H2 # x)) = ((H1 - H2) # x) by FUNCT_2: 63;

 now

 let n be Element of NAT ;



 thus (((H1 # x) (#) (H2 # x)) . n) = (((H1 # x) . n) * ((H2 # x) . n)) by SEQ_1: 8

 .= (((H1 . n) . x) * ((H2 # x) . n)) by Def10

 .= (((H1 . n) . x) * ((H2 . n) . x)) by Def10

 .= (((H1 . n) (#) (H2 . n)) . x) by VALUED_1: 5

 .= (((H1 (#) H2) . n) . x) by Def7

 .= (((H1 (#) H2) # x) . n) by Def10;

 end;

 hence thesis by FUNCT_2: 63;

 end;

 theorem :: SEQFUNC:29



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

 proof

 now

 let n be Element of NAT ;



 thus ((( abs H) # x) . n) = ((( abs H) . n) . x) by Def10

 .= ( |.(H . n).| . x) by Def4

 .= |.((H . n) . x).| by VALUED_1: 18

 .= |.((H # x) . n).| by Def10

 .= (( abs (H # x)) . n) by SEQ_1: 12;

 end;

 hence (( abs H) # x) = ( abs (H # x)) by FUNCT_2: 63;

 now

 let n be Element of NAT ;



 thus ((( - H) # x) . n) = ((( - H) . n) . x) by Def10

 .= (( - (H . n)) . x) by Def3

 .= ( - ((H . n) . x)) by VALUED_1: 8

 .= ( - ((H # x) . n)) by Def10

 .= (( - (H # x)) . n) by SEQ_1: 10;

 end;

 hence thesis by FUNCT_2: 63;

 end;

 theorem :: SEQFUNC:30



 Th29: {x} common_on_dom H implies ((r (#) H) # x) = (r (#) (H # x))

 proof

 assume

 A1: {x} common_on_dom H;

 now

 let n be Element of NAT ;

 x in {x} & {x} c= ( dom (H . n)) by A1, TARSKI:def 1;

 then x in ( dom (H . n));

 then

 A2: x in ( dom (r (#) (H . n))) by VALUED_1:def 5;



 thus (((r (#) H) # x) . n) = (((r (#) H) . n) . x) by Def10

 .= ((r (#) (H . n)) . x) by Def1

 .= (r * ((H . n) . x)) by A2, VALUED_1:def 5

 .= (r * ((H # x) . n)) by Def10

 .= ((r (#) (H # x)) . n) by SEQ_1: 9;

 end;

 hence thesis by FUNCT_2: 63;

 end;

 theorem :: SEQFUNC:31



 Th30: X common_on_dom H1 & X common_on_dom H2 implies for x 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

 assume

 A1: X common_on_dom H1 & X common_on_dom H2;

 let x;

 assume x in X;

 then {x} common_on_dom H1 & {x} common_on_dom H2 by A1, Th25;

 hence thesis by Th27;

 end;

 theorem :: SEQFUNC:32



 Th31: (( abs H) # x) = ( abs (H # x)) & (( - H) # x) = ( - (H # x)) by Th28;

 theorem :: SEQFUNC:33



 Th32: X common_on_dom H implies for x st x in X holds ((r (#) H) # x) = (r (#) (H # x))

 proof

 assume

 A1: X common_on_dom H;

 let x;

 assume x in X;

 then {x} common_on_dom H by A1, Th25;

 hence thesis by Th29;

 end;

 theorem :: SEQFUNC:34



 Th33: H1 is_point_conv_on X & H2 is_point_conv_on X implies for x 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

 (( abs H) # x) = ( abs (H # x)) & (( - H) # x) = ( - (H # x)) by Th31;

 theorem :: SEQFUNC:36

 H is_point_conv_on X implies for x st x in X holds ((r (#) H) # x) = (r (#) (H # x)) by Th32;

 theorem :: SEQFUNC:37



 Th36: X common_on_dom H1 & X common_on_dom H2 implies X common_on_dom (H1 + H2) & X common_on_dom (H1 - H2) & X common_on_dom (H1 (#) H2)

 proof

 assume that

 A1: X common_on_dom H1 and

 A2: X common_on_dom H2;



 A3: X <> {} by A1;

 now

 let n;

 X c= ( dom (H1 . n)) & X c= ( dom (H2 . n)) by A1, A2;

 then X c= (( dom (H1 . n)) /\ ( dom (H2 . n))) by XBOOLE_1: 19;

 then X c= ( dom ((H1 . n) + (H2 . n))) by VALUED_1:def 1;

 hence X c= ( dom ((H1 + H2) . n)) by Def5;

 end;

 hence X common_on_dom (H1 + H2) by A3;

 now

 let n;

 X c= ( dom (H1 . n)) & X c= ( dom (H2 . n)) by A1, A2;

 then X c= (( dom (H1 . n)) /\ ( dom (H2 . n))) by XBOOLE_1: 19;

 then X c= ( dom ((H1 . n) - (H2 . n))) by VALUED_1: 12;

 hence X c= ( dom ((H1 - H2) . n)) by Th3;

 end;

 hence X common_on_dom (H1 - H2) by A3;

 now

 let n;

 X c= ( dom (H1 . n)) & X c= ( dom (H2 . n)) by A1, A2;

 then X c= (( dom (H1 . n)) /\ ( dom (H2 . n))) by XBOOLE_1: 19;

 then X c= ( dom ((H1 . n) (#) (H2 . n))) by VALUED_1:def 4;

 hence X c= ( dom ((H1 (#) H2) . n)) by Def7;

 end;

 hence thesis by A3;

 end;

 theorem :: SEQFUNC:38



 Th37: X common_on_dom H implies X common_on_dom ( abs H) & X common_on_dom ( - H)

 proof

 assume

 A1: X common_on_dom H;

 then

 A2: X <> {} ;

 now

 let n;

 ( dom (H . n)) = ( dom |.(H . n).|) by VALUED_1:def 11

 .= ( dom (( abs H) . n)) by Def4;

 hence X c= ( dom (( abs H) . n)) by A1;

 end;

 hence X common_on_dom ( abs H) by A2;

 now

 let n;

 ( dom (H . n)) = ( dom ( - (H . n))) by VALUED_1: 8

 .= ( dom (( - H) . n)) by Def3;

 hence X c= ( dom (( - H) . n)) by A1;

 end;

 hence thesis by A2;

 end;

 theorem :: SEQFUNC:39



 Th38: X common_on_dom H implies X common_on_dom (r (#) H)

 proof

 assume

 A1: X common_on_dom H;

 A2:

 now

 let n;

 ( dom (H . n)) = ( dom (r (#) (H . n))) by VALUED_1:def 5

 .= ( dom ((r (#) H) . n)) by Def1;

 hence X c= ( dom ((r (#) H) . n)) by A1;

 end;

 X <> {} by A1;

 hence thesis by A2;

 end;

 theorem :: SEQFUNC:40

 H1 is_point_conv_on X & H2 is_point_conv_on X implies (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

 assume that

 A1: H1 is_point_conv_on X and

 A2: H2 is_point_conv_on X;

 A3:

 now

 let x;

 assume

 A4: x in X;

 then (H1 # x) is convergent & (H2 # x) is convergent by A1, A2, Th19;

 then ((H1 # x) + (H2 # x)) is convergent by SEQ_2: 5;

 hence ((H1 + H2) # x) is convergent by A1, A2, A4, Th33;

 end;

 A5:

 now

 let x;

 assume

 A6: x in X;

 then (H1 # x) is convergent & (H2 # x) is convergent by A1, A2, Th19;

 then ((H1 # x) - (H2 # x)) is convergent by SEQ_2: 11;

 hence ((H1 - H2) # x) is convergent by A1, A2, A6, Th33;

 end;



 A7: X common_on_dom H1 & X common_on_dom H2 by A1, A2;

 then X common_on_dom (H1 + H2) by Th36;

 hence

 A8: (H1 + H2) is_point_conv_on X by A3, Th19;

 A9:

 now

 let x;

 assume

 A10: x in ( dom (( lim (H1,X)) + ( lim (H2,X))));

 then

 A11: x in (( dom ( lim (H1,X))) /\ ( dom ( lim (H2,X)))) by VALUED_1:def 1;

 then

 A12: x in ( dom ( lim (H2,X))) by XBOOLE_0:def 4;



 A13: x in ( dom ( lim (H1,X))) by A11, XBOOLE_0:def 4;

 then

 A14: x in X by A1, Def13;

 then

 A15: (H1 # x) is convergent & (H2 # x) is convergent by A1, A2, Th19;



 thus ((( lim (H1,X)) + ( lim (H2,X))) . x) = ((( lim (H1,X)) . x) + (( lim (H2,X)) . x)) by A10, VALUED_1:def 1

 .= (( lim (H1 # x)) + (( lim (H2,X)) . x)) by A1, A13, Def13

 .= (( lim (H1 # x)) + ( lim (H2 # x))) by A2, A12, Def13

 .= ( lim ((H1 # x) + (H2 # x))) by A15, SEQ_2: 6

 .= ( lim ((H1 + H2) # x)) by A1, A2, A14, Th33;

 end;

 A16:

 now

 let x;

 assume

 A17: x in X;

 then (H1 # x) is convergent & (H2 # x) is convergent by A1, A2, Th19;

 then ((H1 # x) (#) (H2 # x)) is convergent by SEQ_2: 14;

 hence ((H1 (#) H2) # x) is convergent by A1, A2, A17, Th33;

 end;

 A18:

 now

 let x;

 assume x in ( dom (( lim (H1,X)) (#) ( lim (H2,X))));

 then

 A19: x in (( dom ( lim (H1,X))) /\ ( dom ( lim (H2,X)))) by VALUED_1:def 4;

 then

 A20: x in ( dom ( lim (H2,X))) by XBOOLE_0:def 4;



 A21: x in ( dom ( lim (H1,X))) by A19, XBOOLE_0:def 4;

 then

 A22: x in X by A1, Def13;

 then

 A23: (H1 # x) is convergent & (H2 # x) is convergent by A1, A2, Th19;



 thus ((( lim (H1,X)) (#) ( lim (H2,X))) . x) = ((( lim (H1,X)) . x) * (( lim (H2,X)) . x)) by VALUED_1: 5

 .= (( lim (H1 # x)) * (( lim (H2,X)) . x)) by A1, A21, Def13

 .= (( lim (H1 # x)) * ( lim (H2 # x))) by A2, A20, Def13

 .= ( lim ((H1 # x) (#) (H2 # x))) by A23, SEQ_2: 15

 .= ( lim ((H1 (#) H2) # x)) by A1, A2, A22, Th33;

 end;

 A24:

 now

 let x;

 assume

 A25: x in ( dom (( lim (H1,X)) - ( lim (H2,X))));

 then

 A26: x in (( dom ( lim (H1,X))) /\ ( dom ( lim (H2,X)))) by VALUED_1: 12;

 then

 A27: x in ( dom ( lim (H2,X))) by XBOOLE_0:def 4;



 A28: x in ( dom ( lim (H1,X))) by A26, XBOOLE_0:def 4;

 then

 A29: x in X by A1, Def13;

 then

 A30: (H1 # x) is convergent & (H2 # x) is convergent by A1, A2, Th19;



 thus ((( lim (H1,X)) - ( lim (H2,X))) . x) = ((( lim (H1,X)) . x) - (( lim (H2,X)) . x)) by A25, VALUED_1: 13

 .= (( lim (H1 # x)) - (( lim (H2,X)) . x)) by A1, A28, Def13

 .= (( lim (H1 # x)) - ( lim (H2 # x))) by A2, A27, Def13

 .= ( lim ((H1 # x) - (H2 # x))) by A30, SEQ_2: 12

 .= ( lim ((H1 - H2) # x)) by A1, A2, A29, Th33;

 end;

 ( dom (( lim (H1,X)) + ( lim (H2,X)))) = (( dom ( lim (H1,X))) /\ ( dom ( lim (H2,X)))) by VALUED_1:def 1

 .= (X /\ ( dom ( lim (H2,X)))) by A1, Def13

 .= (X /\ X) by A2, Def13

 .= X;

 hence ( lim ((H1 + H2),X)) = (( lim (H1,X)) + ( lim (H2,X))) by A8, A9, Def13;

 X common_on_dom (H1 - H2) by A7, Th36;

 hence

 A31: (H1 - H2) is_point_conv_on X by A5, Th19;

 ( dom (( lim (H1,X)) - ( lim (H2,X)))) = (( dom ( lim (H1,X))) /\ ( dom ( lim (H2,X)))) by VALUED_1: 12

 .= (X /\ ( dom ( lim (H2,X)))) by A1, Def13

 .= (X /\ X) by A2, Def13

 .= X;

 hence ( lim ((H1 - H2),X)) = (( lim (H1,X)) - ( lim (H2,X))) by A31, A24, Def13;

 X common_on_dom (H1 (#) H2) by A7, Th36;

 hence

 A32: (H1 (#) H2) is_point_conv_on X by A16, Th19;

 ( dom (( lim (H1,X)) (#) ( lim (H2,X)))) = (( dom ( lim (H1,X))) /\ ( dom ( lim (H2,X)))) by VALUED_1:def 4

 .= (X /\ ( dom ( lim (H2,X)))) by A1, Def13

 .= (X /\ X) by A2, Def13

 .= X;

 hence thesis by A32, A18, Def13;

 end;

 theorem :: SEQFUNC:41

 H is_point_conv_on X implies ( 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

 assume

 A1: H is_point_conv_on X;

 A2:

 now

 let x;

 assume x in X;

 then (H # x) is convergent by A1, Th19;

 then ( abs (H # x)) is convergent by SEQ_4: 13;

 hence (( abs H) # x) is convergent by Th31;

 end;

 A3:

 now

 let x;

 assume x in ( dom ( - ( lim (H,X))));

 then

 A4: x in ( dom ( lim (H,X))) by VALUED_1: 8;

 then x in X by A1, Def13;

 then

 A5: (H # x) is convergent by A1, Th19;



 thus (( - ( lim (H,X))) . x) = ( - (( lim (H,X)) . x)) by VALUED_1: 8

 .= ( - ( lim (H # x))) by A1, A4, Def13

 .= ( lim ( - (H # x))) by A5, SEQ_2: 10

 .= ( lim (( - H) # x)) by Th31;

 end;



 A6: X common_on_dom H by A1;

 then X common_on_dom ( abs H) by Th37;

 hence

 A7: ( abs H) is_point_conv_on X by A2, Th19;

 A8:

 now

 let x;

 assume x in ( dom |.( lim (H,X)).|);

 then

 A9: x in ( dom ( lim (H,X))) by VALUED_1:def 11;

 then x in X by A1, Def13;

 then

 A10: (H # x) is convergent by A1, Th19;



 thus ( |.( lim (H,X)).| . x) = |.(( lim (H,X)) . x).| by VALUED_1: 18

 .= |.( lim (H # x)).| by A1, A9, Def13

 .= ( lim |.(H # x).|) by A10, SEQ_4: 14

 .= ( lim (( abs H) # x)) by Th31;

 end;

 A11:

 now

 let x;

 assume x in X;

 then (H # x) is convergent by A1, Th19;

 then ( - (H # x)) is convergent by SEQ_2: 9;

 hence (( - H) # x) is convergent by Th31;

 end;

 ( dom |.( lim (H,X)).|) = ( dom ( lim (H,X))) by VALUED_1:def 11

 .= X by A1, Def13;

 hence ( lim (( abs H),X)) = |.( lim (H,X)).| by A7, A8, Def13;

 X common_on_dom ( - H) by A6, Th37;

 hence

 A12: ( - H) is_point_conv_on X by A11, Th19;

 ( dom ( - ( lim (H,X)))) = ( dom ( lim (H,X))) by VALUED_1: 8

 .= X by A1, Def13;

 hence thesis by A12, A3, Def13;

 end;

 theorem :: SEQFUNC:42

 H is_point_conv_on X implies (r (#) H) is_point_conv_on X & ( lim ((r (#) H),X)) = (r (#) ( lim (H,X)))

 proof

 assume

 A1: H is_point_conv_on X;

 then

 A2: X common_on_dom H;

 A3:

 now

 let x;

 assume

 A4: x in ( dom (r (#) ( lim (H,X))));

 then

 A5: x in ( dom ( lim (H,X))) by VALUED_1:def 5;

 then

 A6: x in X by A1, Def13;

 then

 A7: (H # x) is convergent by A1, Th19;



 thus ((r (#) ( lim (H,X))) . x) = (r * (( lim (H,X)) . x)) by A4, VALUED_1:def 5

 .= (r * ( lim (H # x))) by A1, A5, Def13

 .= ( lim (r (#) (H # x))) by A7, SEQ_2: 8

 .= ( lim ((r (#) H) # x)) by A2, A6, Th32;

 end;

 A8:

 now

 let x;

 assume

 A9: x in X;

 then (H # x) is convergent by A1, Th19;

 then (r (#) (H # x)) is convergent by SEQ_2: 7;

 hence ((r (#) H) # x) is convergent by A2, A9, Th32;

 end;

 X common_on_dom (r (#) H) by A2, Th38;

 hence

 A10: (r (#) H) is_point_conv_on X by A8, Th19;

 ( dom (r (#) ( lim (H,X)))) = ( dom ( lim (H,X))) by VALUED_1:def 5

 .= X by A1, Def13;

 hence thesis by A10, A3, Def13;

 end;

 theorem :: SEQFUNC:43



 Th42: H is_unif_conv_on X iff X common_on_dom H & H is_point_conv_on X & for r st 0 < r holds ex k st for n, x st n >= k & x in X holds |.(((H . n) . x) - (( lim (H,X)) . x)).| < r

 proof

 thus H is_unif_conv_on X implies X common_on_dom H & H is_point_conv_on X & for r st 0 < r holds ex k st for n, x st n >= k & x in X holds |.(((H . n) . x) - (( lim (H,X)) . x)).| < r

 proof

 assume

 A1: H is_unif_conv_on X;

 then

 consider f such that

 A2: X = ( dom f) and

 A3: for p st p > 0 holds ex k st for n, x st n >= k & x in X holds |.(((H . n) . x) - (f . x)).| < p;

 thus X common_on_dom H by A1;

 A4:

 now

 let x such that

 A5: x in X;

 let p;

 assume p > 0 ;

 then

 consider k such that

 A6: for n, x st n >= k & x in X holds |.(((H . n) . x) - (f . x)).| = k;

 hence |.(((H . n) . x) - (f . x)).| 0 ;

 then

 consider k such that

 A8: for n, x st n >= k & x in X holds |.(((H . n) . x) - (f . x)).| < r by A3;

 take k;

 let n, x;

 assume n >= k & x in X;

 hence thesis by A7, A8;

 end;

 assume that

 A9: X common_on_dom H and

 A10: H is_point_conv_on X and

 A11: for r st 0 < r holds ex k st for n, x st n >= k & x in X holds |.(((H . n) . x) - (( lim (H,X)) . x)).| < r;

 ( dom ( lim (H,X))) = X by A10, Def13;

 hence thesis by A9, A11;

 end;

 reserve H for Functional_Sequence of REAL , REAL ;

 theorem :: SEQFUNC:44

 H is_unif_conv_on X & (for n holds ((H . n) | X) is continuous) implies (( lim (H,X)) | X) is continuous

 proof

 set l = ( lim (H,X));

 assume that

 A1: H is_unif_conv_on X and

 A2: for n holds ((H . n) | X) is continuous;



 A3: H is_point_conv_on X by A1, Th21;

 then

 A4: ( dom l) = X by Def13;



 A5: X common_on_dom H by A1;

 for x0 be Real st x0 in ( dom (l | X)) holds (l | X) is_continuous_in x0

 proof

 let x0 be Real;

 assume x0 in ( dom (l | X));

 then

 A6: x0 in X by RELAT_1: 57;

 reconsider x0 as Element of REAL by XREAL_0:def 1;

 for r be Real st 0 < r holds ex s be Real st 0 < s & for x1 be Real st x1 in ( dom (l | X)) & |.(x1 - x0).| < s holds |.(((l | X) . x1) - ((l | X) . x0)).| < r

 proof

 let r be Real;

 assume 0 < r;

 then

 A7: 0 < (r / 3) by XREAL_1: 222;

 reconsider r as Element of REAL by XREAL_0:def 1;

 consider k such that

 A8: for n holds for x1 be Element of REAL st n >= k & x1 in X holds |.(((H . n) . x1) - (l . x1)).| < (r / 3) by A1, A7, Th42;

 consider k1 be Nat such that

 A9: for n st n >= k1 holds |.(((H . n) . x0) - (l . x0)).| < (r / 3) by A3, A6, A7, Th20;

 reconsider m = ( max (k,k1)) as Nat by TARSKI: 1;

 set h = (H . m);



 A10: X c= ( dom h) by A5;



 A11: ( dom (h | X)) = (( dom h) /\ X) by RELAT_1: 61

 .= X by A10, XBOOLE_1: 28;

 (h | X) is continuous by A2;

 then (h | X) is_continuous_in x0 by A6, A11, FCONT_1:def 2;

 then

 consider s be Real such that

 A12: 0 < s and

 A13: for x1 be Real st x1 in ( dom (h | X)) & |.(x1 - x0).| < s holds |.(((h | X) . x1) - ((h | X) . x0)).| < (r / 3) by A7, FCONT_1: 3;

 reconsider s as Real;

 take s;

 thus 0 < s by A12;

 let x1 be Real;

 assume that

 A14: x1 in ( dom (l | X)) and

 A15: |.(x1 - x0).| < s;



 A16: ( dom (l | X)) = (( dom l) /\ X) by RELAT_1: 61

 .= X by A4;

 then |.(((h | X) . x1) - ((h | X) . x0)).| < (r / 3) by A11, A13, A14, A15;

 then |.((h . x1) - ((h | X) . x0)).| < (r / 3) by A16, A11, A14, FUNCT_1: 47;

 then

 A17: |.((h . x1) - (h . x0)).| < (r / 3) by A6, FUNCT_1: 49;

 |.((h . x0) - (l . x0)).| < (r / 3) by A9, XXREAL_0: 25;

 then |.(((h . x1) - (h . x0)) + ((h . x0) - (l . x0))).| <= ( |.((h . x1) - (h . x0)).| + |.((h . x0) - (l . x0)).|) & ( |.((h . x1) - (h . x0)).| + |.((h . x0) - (l . x0)).|) < ((r / 3) + (r / 3)) by A17, COMPLEX1: 56, XREAL_1: 8;

 then

 A18: |.(((h . x1) - (h . x0)) + ((h . x0) - (l . x0))).| < ((r / 3) + (r / 3)) by XXREAL_0: 2;

 |.((l . x1) - (l . x0)).| = |.(((l . x1) - (h . x1)) + (((h . x1) - (h . x0)) + ((h . x0) - (l . x0)))).|;

 then

 A19: |.((l . x1) - (l . x0)).| <= ( |.((l . x1) - (h . x1)).| + |.(((h . x1) - (h . x0)) + ((h . x0) - (l . x0))).|) by COMPLEX1: 56;

 |.((h . x1) - (l . x1)).| < (r / 3) by A8, A16, A14, XXREAL_0: 25;

 then |.( - ((l . x1) - (h . x1))).| < (r / 3);

 then |.((l . x1) - (h . x1)).| < (r / 3) by COMPLEX1: 52;

 then ( |.((l . x1) - (h . x1)).| + |.(((h . x1) - (h . x0)) + ((h . x0) - (l . x0))).|) < ((r / 3) + ((r / 3) + (r / 3))) by A18, XREAL_1: 8;

 then |.((l . x1) - (l . x0)).| < (((r / 3) + (r / 3)) + (r / 3)) by A19, XXREAL_0: 2;

 then |.(((l | X) . x1) - (l . x0)).| < r by A14, FUNCT_1: 47;

 hence thesis by A4, RELAT_1: 68;

 end;

 hence thesis by FCONT_1: 3;

 end;

 hence thesis by FCONT_1:def 2;

 end;