:: SEQFUNC semantic presentation

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
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  F . n is PartFunc of D1,D2 by PARTFUN1:46; ::_thesis: verum
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
let D1, D2 be set ; ::_thesis: 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 ) ) )
let f be Function; ::_thesis: ( 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 ) ) )
thus  ( f is Functional_Sequence of D1,D2 implies ( dom f = NAT & ( for x being set st x in NAT holds
f . x is PartFunc of D1,D2 ) ) ) ::_thesis: ( dom f = NAT & ( for x being set st x in NAT holds
f . x is PartFunc of D1,D2 ) implies f is Functional_Sequence of D1,D2 )
proof
assume A1: f is Functional_Sequence of D1,D2 ; ::_thesis: ( dom f = NAT & ( for x being set st x in NAT holds
f . x is PartFunc of D1,D2 ) )
hence  dom f = NAT by FUNCT_2:def_1; ::_thesis: for x being set st x in NAT holds
f . x is PartFunc of D1,D2
let x be set ; ::_thesis: ( x in NAT implies f . x is PartFunc of D1,D2 )
assume  x in NAT ; ::_thesis: f . x is PartFunc of D1,D2
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  f . x is PartFunc of D1,D2 by A2, PARTFUN1:46; ::_thesis: verum
end;
assume that
A3: dom f = NAT and
A4: for x being set st x in NAT holds
f . x is PartFunc of D1,D2 ; ::_thesis: f is Functional_Sequence of D1,D2
now__::_thesis:_for_y_being_set_st_y_in_rng_f_holds_
y_in_PFuncs_(D1,D2)
let y be set ; ::_thesis: ( y in rng f implies y in PFuncs (D1,D2) )
assume  y in rng f ; ::_thesis: y in PFuncs (D1,D2)
then consider x being set  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; ::_thesis: verum
end;
then  rng f c= PFuncs (D1,D2) by TARSKI:def_3;
hence  f is Functional_Sequence of D1,D2 by A3, FUNCT_2:def_1, RELSET_1:4; ::_thesis: verum
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 Element of NAT holds f . n is PartFunc of D1,D2 ) ) )
proof
let D1, D2 be set ; ::_thesis: 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 ) ) )
let f be Function; ::_thesis: ( 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 ) ) )
thus  ( f is Functional_Sequence of D1,D2 implies ( dom f = NAT & ( for n being Element of NAT holds f . n is PartFunc of D1,D2 ) ) ) by Lm1; ::_thesis: ( dom f = NAT & ( for n being Element of NAT holds f . n is PartFunc of D1,D2 ) implies f is Functional_Sequence of D1,D2 )
assume that
A1: dom f = NAT and
A2: for n being Element of NAT holds f . n is PartFunc of D1,D2 ; ::_thesis: f is Functional_Sequence of D1,D2
 for x being set st x in NAT holds
f . x is PartFunc of D1,D2 by A2;
hence  f is Functional_Sequence of D1,D2 by A1, Lm1; ::_thesis: verum
end;

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)
proof
defpred S1[ set , set ] means $2 = F3($1);
A1: for x being set st x in NAT holds
ex y being set st S1[x,y] ;
consider f being Function such that
A2: dom f = NAT and
A3: for x being set st x in NAT holds
S1[x,f . x] from CLASSES1:sch_1(A1);
now__::_thesis:_for_x_being_set_st_x_in_NAT_holds_
f_._x_is_PartFunc_of_F1(),F2()
let x be set ; ::_thesis: ( x in NAT implies f . x is PartFunc of F1(),F2() )
assume  x in NAT ; ::_thesis: f . x is PartFunc of F1(),F2()
then  f . x = F3(x) by A3;
hence  f . x is PartFunc of F1(),F2() ; ::_thesis: verum
end;
then reconsider f = f as Functional_Sequence of F1(),F2() by A2, Lm1;
take  f ; ::_thesis: for n being Nat holds f . n = F3(n)
let n be Nat; ::_thesis: f . n = F3(n)
 n in NAT by ORDINAL1:def_12;
hence  f . n = F3(n) by A3; ::_thesis: verum
end;

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)
proof
deffunc H1( Nat) ->  Element of K19(K20(D,REAL)) = r (#) (H . $1);
thus  ex f being Functional_Sequence of D,REAL st
for n being Nat holds f . n = H1(n) from SEQFUNC:sch_1(); ::_thesis: verum
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
let H1, H2 be Functional_Sequence of D,REAL; ::_thesis: ( ( for n being Nat holds H1 . n = r (#) (H . n) ) & ( for n being Nat holds H2 . n = r (#) (H . n) ) implies H1 = H2 )
assume that
A1: for n being Nat holds H1 . n = r (#) (H . n) and
A2: for n being Nat holds H2 . n = r (#) (H . n) ; ::_thesis: H1 = H2
now__::_thesis:_for_n_being_Element_of_NAT_holds_H1_._n_=_H2_._n
let n be Element of NAT ; ::_thesis: H1 . n = H2 . n
 H1 . n = r (#) (H . n) by A1;
hence  H1 . n = H2 . n by A2; ::_thesis: verum
end;
hence  H1 = H2 by FUNCT_2:63; ::_thesis: verum
end;
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) ^
proof
deffunc H1( Nat) ->  Element of K19(K20(D,REAL)) = (H . $1) ^ ;
thus  ex f being Functional_Sequence of D,REAL st
for n being Nat holds f . n = H1(n) from SEQFUNC:sch_1(); ::_thesis: verum
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
let H1, H2 be Functional_Sequence of D,REAL; ::_thesis: ( ( for n being Nat holds H1 . n = (H . n) ^ ) & ( for n being Nat holds H2 . n = (H . n) ^ ) implies H1 = H2 )
assume that
A1: for n being Nat holds H1 . n = (H . n) ^ and
A2: for n being Nat holds H2 . n = (H . n) ^ ; ::_thesis: H1 = H2
now__::_thesis:_for_n_being_Element_of_NAT_holds_H1_._n_=_H2_._n
let n be Element of NAT ; ::_thesis: H1 . n = H2 . n
 H1 . n = (H . n) ^ by A1;
hence  H1 . n = H2 . n by A2; ::_thesis: verum
end;
hence  H1 = H2 by FUNCT_2:63; ::_thesis: verum
end;
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
take  (- 1) (#) H ; ::_thesis: for n being Nat holds ((- 1) (#) H) . n = - (H . n)
let n be Nat; ::_thesis: ((- 1) (#) H) . n = - (H . n)
thus  ((- 1) (#) H) . n = - (H . n) by Def1; ::_thesis: verum
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
let H1, H2 be Functional_Sequence of D,REAL; ::_thesis: ( ( for n being Nat holds H1 . n = - (H . n) ) & ( for n being Nat holds H2 . n = - (H . n) ) implies H1 = H2 )
assume that
A3: for n being Nat holds H1 . n = - (H . n) and
A4: for n being Nat holds H2 . n = - (H . n) ; ::_thesis: H1 = H2
now__::_thesis:_for_n_being_Element_of_NAT_holds_H1_._n_=_H2_._n
let n be Element of NAT ; ::_thesis: H1 . n = H2 . n
 H1 . n = - (H . n) by A3;
hence  H1 . n = H2 . n by A4; ::_thesis: verum
end;
hence  H1 = H2 by FUNCT_2:63; ::_thesis: verum
end;
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)
proof
let G, H be Functional_Sequence of D,REAL; ::_thesis: ( ( for n being Nat holds G . n = - (H . n) ) implies for n being Nat holds H . n = - (G . n) )
assume A5: for n being Nat holds G . n = - (H . n) ; ::_thesis: for n being Nat holds H . n = - (G . n)
let n be Nat; ::_thesis: H . n = - (G . n)
thus H . n = - (- (H . n))
.= - (G . n) by A5 ; ::_thesis: verum
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
 ex b1 being Functional_Sequence of D,REAL st
for n being Nat holds b1 . n = abs (H . n)
proof
deffunc H1( Nat) ->  Element of K19(K20(D,REAL)) = abs (H . $1);
thus  ex f being Functional_Sequence of D,REAL st
for n being Nat holds f . n = H1(n) from SEQFUNC:sch_1(); ::_thesis: verum
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
let H1, H2 be Functional_Sequence of D,REAL; ::_thesis: ( ( for n being Nat holds H1 . n = abs (H . n) ) & ( for n being Nat holds H2 . n = abs (H . n) ) implies H1 = H2 )
assume that
A6: for n being Nat holds H1 . n = abs (H . n) and
A7: for n being Nat holds H2 . n = abs (H . n) ; ::_thesis: H1 = H2
now__::_thesis:_for_n_being_Element_of_NAT_holds_H1_._n_=_H2_._n
let n be Element of NAT ; ::_thesis: H1 . n = H2 . n
 H2 . n = abs (H . n) by A7;
hence  H1 . n = H2 . n by A6; ::_thesis: verum
end;
hence  H1 = H2 by FUNCT_2:63; ::_thesis: verum
end;
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)
proof
let G, H be Functional_Sequence of D,REAL; ::_thesis: ( ( for n being Nat holds G . n = abs (H . n) ) implies for n being Nat holds G . n = abs (G . n) )
assume A8: for n being Nat holds G . n = abs (H . n) ; ::_thesis: for n being Nat holds G . n = abs (G . n)
let n be Nat; ::_thesis: G . n = abs (G . n)
thus G . n = abs (abs (H . n)) by A8
.= abs (G . n) by A8 ; ::_thesis: verum
end;
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)
proof
deffunc H1( Nat) ->  Element of K19(K20(D,REAL)) = (G . $1) + (H . $1);
thus  ex f being Functional_Sequence of D,REAL st
for n being Nat holds f . n = H1(n) from SEQFUNC:sch_1(); ::_thesis: verum
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
let H1, H2 be Functional_Sequence of D,REAL; ::_thesis: ( ( for n being Nat holds H1 . n = (G . n) + (H . n) ) & ( for n being Nat holds H2 . n = (G . n) + (H . n) ) implies H1 = H2 )
assume that
A1: for n being Nat holds H1 . n = (G . n) + (H . n) and
A2: for n being Nat holds H2 . n = (G . n) + (H . n) ; ::_thesis: H1 = H2
now__::_thesis:_for_n_being_Element_of_NAT_holds_H1_._n_=_H2_._n
let n be Element of NAT ; ::_thesis: H1 . n = H2 . n
 H1 . n = (G . n) + (H . n) by A1;
hence  H1 . n = H2 . n by A2; ::_thesis: verum
end;
hence  H1 = H2 by FUNCT_2:63; ::_thesis: verum
end;
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)
proof
deffunc H1( Nat) ->  Element of K19(K20(D,REAL)) = (G . $1) (#) (H . $1);
thus  ex f being Functional_Sequence of D,REAL st
for n being Nat holds f . n = H1(n) from SEQFUNC:sch_1(); ::_thesis: verum
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
let H1, H2 be Functional_Sequence of D,REAL; ::_thesis: ( ( for n being Nat holds H1 . n = (G . n) (#) (H . n) ) & ( for n being Nat holds H2 . n = (G . n) (#) (H . n) ) implies H1 = H2 )
assume that
A1: for n being Nat holds H1 . n = (G . n) (#) (H . n) and
A2: for n being Nat holds H2 . n = (G . n) (#) (H . n) ; ::_thesis: H1 = H2
now__::_thesis:_for_n_being_Element_of_NAT_holds_H1_._n_=_H2_._n
let n be Element of NAT ; ::_thesis: H1 . n = H2 . n
 H1 . n = (G . n) (#) (H . n) by A1;
hence  H1 . n = H2 . n by A2; ::_thesis: verum
end;
hence  H1 = H2 by FUNCT_2:63; ::_thesis: verum
end;
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) )
proof
let D be non empty set ; ::_thesis: 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) )
let H1, G, H be Functional_Sequence of D,REAL; ::_thesis: ( H1 = G / H iff for n being Element of NAT holds H1 . n = (G . n) / (H . n) )
thus  ( H1 = G / H implies for n being Element of NAT holds H1 . n = (G . n) / (H . n) ) ::_thesis: ( ( for n being Element of NAT holds H1 . n = (G . n) / (H . n) ) implies H1 = G / H )
proof
assume A1: H1 = G / H ; ::_thesis: for n being Element of NAT holds H1 . n = (G . n) / (H . n)
let n be Element of NAT ; ::_thesis: H1 . n = (G . n) / (H . 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 ; ::_thesis: verum
end;
assume A2: for n being Element of NAT holds H1 . n = (G . n) / (H . n) ; ::_thesis: H1 = G / H
now__::_thesis:_for_n_being_Element_of_NAT_holds_H1_._n_=_(G_/_H)_._n
let n be Element of NAT ; ::_thesis: H1 . n = (G / H) . n
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 ; ::_thesis: verum
end;
hence  H1 = G / H by FUNCT_2:63; ::_thesis: verum
end;

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) )
proof
let D be non empty set ; ::_thesis: 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) )
let H1, G, H be Functional_Sequence of D,REAL; ::_thesis: ( H1 = G - H iff for n being Element of NAT holds H1 . n = (G . n) - (H . n) )
thus  ( H1 = G - H implies for n being Element of NAT holds H1 . n = (G . n) - (H . n) ) ::_thesis: ( ( for n being Element of NAT holds H1 . n = (G . n) - (H . n) ) implies H1 = G - H )
proof
assume A1: H1 = G - H ; ::_thesis: for n being Element of NAT holds H1 . n = (G . n) - (H . n)
let n be Element of NAT ; ::_thesis: H1 . n = (G . n) - (H . n)
thus H1 . n = (G . n) + ((- H) . n) by A1, Def5
.= (G . n) - (H . n) by Def3 ; ::_thesis: verum
end;
assume A2: for n being Element of NAT holds H1 . n = (G . n) - (H . n) ; ::_thesis: H1 = G - H
now__::_thesis:_for_n_being_Element_of_NAT_holds_H1_._n_=_(G_-_H)_._n
let n be Element of NAT ; ::_thesis: H1 . n = (G - H) . n
thus H1 . n = (G . n) - (H . n) by A2
.= (G . n) + ((- H) . n) by Def3
.= (G - H) . n by Def5 ; ::_thesis: verum
end;
hence  H1 = G - H by FUNCT_2:63; ::_thesis: verum
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) )
proof
let D be non empty set ; ::_thesis: for G, H, J being Functional_Sequence of D,REAL holds
( G + H = H + G & (G + H) + J = G + (H + J) )
let G, H, J be Functional_Sequence of D,REAL; ::_thesis: ( G + H = H + G & (G + H) + J = G + (H + J) )
now__::_thesis:_for_n_being_Element_of_NAT_holds_(G_+_H)_._n_=_(H_+_G)_._n
let n be Element of NAT ; ::_thesis: (G + H) . n = (H + G) . n
thus (G + H) . n = (H . n) + (G . n) by Def5
.= (H + G) . n by Def5 ; ::_thesis: verum
end;
hence  G + H = H + G by FUNCT_2:63; ::_thesis: (G + H) + J = G + (H + J)
now__::_thesis:_for_n_being_Element_of_NAT_holds_((G_+_H)_+_J)_._n_=_(G_+_(H_+_J))_._n
let n be Element of NAT ; ::_thesis: ((G + H) + J) . n = (G + (H + J)) . n
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 ; ::_thesis: verum
end;
hence  (G + H) + J = G + (H + J) by FUNCT_2:63; ::_thesis: verum
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) )
proof
let D be non empty set ; ::_thesis: for G, H, J being Functional_Sequence of D,REAL holds
( G (#) H = H (#) G & (G (#) H) (#) J = G (#) (H (#) J) )
let G, H, J be Functional_Sequence of D,REAL; ::_thesis: ( G (#) H = H (#) G & (G (#) H) (#) J = G (#) (H (#) J) )
now__::_thesis:_for_n_being_Element_of_NAT_holds_(G_(#)_H)_._n_=_(H_(#)_G)_._n
let n be Element of NAT ; ::_thesis: (G (#) H) . n = (H (#) G) . n
thus (G (#) H) . n = (H . n) (#) (G . n) by Def7
.= (H (#) G) . n by Def7 ; ::_thesis: verum
end;
hence  G (#) H = H (#) G by FUNCT_2:63; ::_thesis: (G (#) H) (#) J = G (#) (H (#) J)
now__::_thesis:_for_n_being_Element_of_NAT_holds_((G_(#)_H)_(#)_J)_._n_=_(G_(#)_(H_(#)_J))_._n
let n be Element of NAT ; ::_thesis: ((G (#) H) (#) J) . n = (G (#) (H (#) J)) . n
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 ; ::_thesis: verum
end;
hence  (G (#) H) (#) J = G (#) (H (#) J) by FUNCT_2:63; ::_thesis: verum
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) )
proof
let D be non empty set ; ::_thesis: 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) )
let G, H, J be Functional_Sequence of D,REAL; ::_thesis: ( (G + H) (#) J = (G (#) J) + (H (#) J) & J (#) (G + H) = (J (#) G) + (J (#) H) )
now__::_thesis:_for_n_being_Element_of_NAT_holds_((G_+_H)_(#)_J)_._n_=_((G_(#)_J)_+_(H_(#)_J))_._n
let n be Element of NAT ; ::_thesis: ((G + H) (#) J) . n = ((G (#) J) + (H (#) J)) . n
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 ; ::_thesis: verum
end;
hence  (G + H) (#) J = (G (#) J) + (H (#) J) by FUNCT_2:63; ::_thesis: J (#) (G + H) = (J (#) G) + (J (#) H)
hence J (#) (G + H) = (G (#) J) + (H (#) J) by Th5
.= (J (#) G) + (H (#) J) by Th5
.= (J (#) G) + (J (#) H) by Th5 ;
::_thesis: verum
end;

theorem :: SEQFUNC:7
for D being non empty set
for H being Functional_Sequence of D,REAL holds - H = (- 1) (#) H
proof
let D be non empty set ; ::_thesis: for H being Functional_Sequence of D,REAL holds - H = (- 1) (#) H
let H be Functional_Sequence of D,REAL; ::_thesis: - H = (- 1) (#) H
now__::_thesis:_for_n_being_Element_of_NAT_holds_(-_H)_._n_=_((-_1)_(#)_H)_._n
let n be Element of NAT ; ::_thesis: (- H) . n = ((- 1) (#) H) . n
thus (- H) . n = - (H . n) by Def3
.= ((- 1) (#) H) . n by Def1 ; ::_thesis: verum
end;
hence  - H = (- 1) (#) H by FUNCT_2:63; ::_thesis: verum
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) )
proof
let D be non empty set ; ::_thesis: 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) )
let G, H, J be Functional_Sequence of D,REAL; ::_thesis: ( (G - H) (#) J = (G (#) J) - (H (#) J) & (J (#) G) - (J (#) H) = J (#) (G - H) )
now__::_thesis:_for_n_being_Element_of_NAT_holds_((G_-_H)_(#)_J)_._n_=_((G_(#)_J)_-_(H_(#)_J))_._n
let n be Element of NAT ; ::_thesis: ((G - H) (#) J) . n = ((G (#) J) - (H (#) J)) . n
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 ; ::_thesis: verum
end;
hence A1: (G - H) (#) J = (G (#) J) - (H (#) J) by FUNCT_2:63; ::_thesis: (J (#) G) - (J (#) H) = J (#) (G - H)
thus (J (#) G) - (J (#) H) = (J (#) G) - (H (#) J) by Th5
.= (G - H) (#) J by A1, Th5
.= J (#) (G - H) by Th5 ; ::_thesis: verum
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) )
proof
let D be non empty set ; ::_thesis: 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) )
let r be Real; ::_thesis: for G, H being Functional_Sequence of D,REAL holds
( r (#) (G + H) = (r (#) G) + (r (#) H) & r (#) (G - H) = (r (#) G) - (r (#) H) )
let G, H be Functional_Sequence of D,REAL; ::_thesis: ( r (#) (G + H) = (r (#) G) + (r (#) H) & r (#) (G - H) = (r (#) G) - (r (#) H) )
now__::_thesis:_for_n_being_Element_of_NAT_holds_(r_(#)_(G_+_H))_._n_=_((r_(#)_G)_+_(r_(#)_H))_._n
let n be Element of NAT ; ::_thesis: (r (#) (G + H)) . n = ((r (#) G) + (r (#) H)) . n
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 ; ::_thesis: verum
end;
hence  r (#) (G + H) = (r (#) G) + (r (#) H) by FUNCT_2:63; ::_thesis: r (#) (G - H) = (r (#) G) - (r (#) H)
now__::_thesis:_for_n_being_Element_of_NAT_holds_(r_(#)_(G_-_H))_._n_=_((r_(#)_G)_-_(r_(#)_H))_._n
let n be Element of NAT ; ::_thesis: (r (#) (G - H)) . n = ((r (#) G) - (r (#) H)) . n
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 ; ::_thesis: verum
end;
hence  r (#) (G - H) = (r (#) G) - (r (#) H) by FUNCT_2:63; ::_thesis: verum
end;

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)
proof
let D be non empty set ; ::_thesis: for r, p being Real
for H being Functional_Sequence of D,REAL holds (r * p) (#) H = r (#) (p (#) H)
let r, p be Real; ::_thesis: for H being Functional_Sequence of D,REAL holds (r * p) (#) H = r (#) (p (#) H)
let H be Functional_Sequence of D,REAL; ::_thesis: (r * p) (#) H = r (#) (p (#) H)
now__::_thesis:_for_n_being_Element_of_NAT_holds_((r_*_p)_(#)_H)_._n_=_(r_(#)_(p_(#)_H))_._n
let n be Element of NAT ; ::_thesis: ((r * p) (#) H) . n = (r (#) (p (#) H)) . n
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 ; ::_thesis: verum
end;
hence  (r * p) (#) H = r (#) (p (#) H) by FUNCT_2:63; ::_thesis: verum
end;

theorem :: SEQFUNC:11
for D being non empty set
for H being Functional_Sequence of D,REAL holds 1 (#) H = H
proof
let D be non empty set ; ::_thesis: for H being Functional_Sequence of D,REAL holds 1 (#) H = H
let H be Functional_Sequence of D,REAL; ::_thesis: 1 (#) H = H
now__::_thesis:_for_n_being_Element_of_NAT_holds_(1_(#)_H)_._n_=_H_._n
let n be Element of NAT ; ::_thesis: (1 (#) H) . n = H . n
thus (1 (#) H) . n = 1 (#) (H . n) by Def1
.= H . n by RFUNCT_1:21 ; ::_thesis: verum
end;
hence  1 (#) H = H by FUNCT_2:63; ::_thesis: verum
end;

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) "
proof
let D be non empty set ; ::_thesis: for G, H being Functional_Sequence of D,REAL holds (G ") (#) (H ") = (G (#) H) "
let G, H be Functional_Sequence of D,REAL; ::_thesis: (G ") (#) (H ") = (G (#) H) "
now__::_thesis:_for_n_being_Element_of_NAT_holds_((G_")_(#)_(H_"))_._n_=_((G_(#)_H)_")_._n
let n be Element of NAT ; ::_thesis: ((G ") (#) (H ")) . n = ((G (#) H) ") . n
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 ; ::_thesis: verum
end;
hence  (G ") (#) (H ") = (G (#) H) " by FUNCT_2:63; ::_thesis: verum
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 ")
proof
let D be non empty set ; ::_thesis: for r being Real
for H being Functional_Sequence of D,REAL st r <> 0 holds
(r (#) H) " = (r ") (#) (H ")
let r be Real; ::_thesis: for H being Functional_Sequence of D,REAL st r <> 0 holds
(r (#) H) " = (r ") (#) (H ")
let H be Functional_Sequence of D,REAL; ::_thesis: ( r <> 0 implies (r (#) H) " = (r ") (#) (H ") )
assume A1: r <> 0 ; ::_thesis: (r (#) H) " = (r ") (#) (H ")
now__::_thesis:_for_n_being_Element_of_NAT_holds_((r_(#)_H)_")_._n_=_((r_")_(#)_(H_"))_._n
let n be Element of NAT ; ::_thesis: ((r (#) H) ") . n = ((r ") (#) (H ")) . n
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 ; ::_thesis: verum
end;
hence  (r (#) H) " = (r ") (#) (H ") by FUNCT_2:63; ::_thesis: verum
end;

theorem Th15: :: SEQFUNC:15
for D being non empty set
for H being Functional_Sequence of D,REAL holds (abs H) " = abs (H ")
proof
let D be non empty set ; ::_thesis: for H being Functional_Sequence of D,REAL holds (abs H) " = abs (H ")
let H be Functional_Sequence of D,REAL; ::_thesis: (abs H) " = abs (H ")
now__::_thesis:_for_n_being_Element_of_NAT_holds_(abs_(H_"))_._n_=_((abs_H)_")_._n
let n be Element of NAT ; ::_thesis: (abs (H ")) . n = ((abs H) ") . n
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 ; ::_thesis: verum
end;
hence  (abs H) " = abs (H ") by FUNCT_2:63; ::_thesis: verum
end;

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)
proof
let D be non empty set ; ::_thesis: for G, H being Functional_Sequence of D,REAL holds abs (G (#) H) = (abs G) (#) (abs H)
let G, H be Functional_Sequence of D,REAL; ::_thesis: abs (G (#) H) = (abs G) (#) (abs H)
now__::_thesis:_for_n_being_Element_of_NAT_holds_(abs_(G_(#)_H))_._n_=_((abs_G)_(#)_(abs_H))_._n
let n be Element of NAT ; ::_thesis: (abs (G (#) H)) . n = ((abs G) (#) (abs H)) . n
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 ; ::_thesis: verum
end;
hence  abs (G (#) H) = (abs G) (#) (abs H) by FUNCT_2:63; ::_thesis: verum
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)
proof
let D be non empty set ; ::_thesis: for G, H being Functional_Sequence of D,REAL holds abs (G / H) = (abs G) / (abs H)
let G, H be Functional_Sequence of D,REAL; ::_thesis: abs (G / H) = (abs G) / (abs H)
thus  abs (G / H) = (abs G) (#) (abs (H ")) by Th16
.= (abs G) / (abs H) by Th15 ; ::_thesis: verum
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) = (abs r) (#) (abs H)
proof
let D be non empty set ; ::_thesis: for r being Real
for H being Functional_Sequence of D,REAL holds abs (r (#) H) = (abs r) (#) (abs H)
let r be Real; ::_thesis: for H being Functional_Sequence of D,REAL holds abs (r (#) H) = (abs r) (#) (abs H)
let H be Functional_Sequence of D,REAL; ::_thesis: abs (r (#) H) = (abs r) (#) (abs H)
now__::_thesis:_for_n_being_Element_of_NAT_holds_(abs_(r_(#)_H))_._n_=_((abs_r)_(#)_(abs_H))_._n
let n be Element of NAT ; ::_thesis: (abs (r (#) H)) . n = ((abs r) (#) (abs H)) . n
thus (abs (r (#) H)) . n = abs ((r (#) H) . n) by Def4
.= abs (r (#) (H . n)) by Def1
.= (abs r) (#) (abs (H . n)) by RFUNCT_1:25
.= (abs r) (#) ((abs H) . n) by Def4
.= ((abs r) (#) (abs H)) . n by Def1 ; ::_thesis: verum
end;
hence  abs (r (#) H) = (abs r) (#) (abs H) by FUNCT_2:63; ::_thesis: verum
end;


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 <> {} & ( 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 <> {} & ( 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
proof
deffunc H1( Element of NAT ) ->  Element of REAL = (H . $1) . x;
thus  ex f being Real_Sequence st
for n being Element of NAT holds f . n = H1(n) from SEQ_1:sch_1(); ::_thesis: verum
end;
uniqueness
 for b1, b2 being Real_Sequence st ( for n being Element of NAT holds b1 . n = (H . n) . x ) & ( for n being Element of NAT holds b2 . n = (H . n) . x ) holds
b1 = b2
proof
let S1, S2 be Real_Sequence; ::_thesis: ( ( for n being Element of NAT holds S1 . n = (H . n) . x ) & ( for n being Element of NAT holds S2 . n = (H . n) . x ) implies S1 = S2 )
assume that
A1: for n being Element of NAT holds S1 . n = (H . n) . x and
A2: for n being Element of NAT holds S2 . n = (H . n) . x ; ::_thesis: S1 = S2
now__::_thesis:_for_n_being_Element_of_NAT_holds_S1_._n_=_S2_._n
let n be Element of NAT ; ::_thesis: S1 . n = S2 . n
 S1 . n = (H . n) . x by A1;
hence  S1 . n = S2 . n by A2; ::_thesis: verum
end;
hence  S1 = S2 by FUNCT_2:63; ::_thesis: verum
end;
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 & 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 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 & 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 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 & 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
let D be non empty set ; ::_thesis: 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 ) ) ) ) )
let H be Functional_Sequence of D,REAL; ::_thesis: 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 ) ) ) ) )
let X be set ; ::_thesis: ( 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 ) ) ) ) )
thus  ( H is_point_conv_on X implies ( 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 ) ) ) ) ) ::_thesis: ( 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 ) ) ) implies H is_point_conv_on X )
proof
assume A1: H is_point_conv_on X ; ::_thesis: ( 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 ) ) ) )
hence  X common_on_dom H by Def11; ::_thesis: 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 ) ) )
consider f being PartFunc of D,REAL such that
A2: X = dom f and
A3: 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 by A1, Def11;
take  f ; ::_thesis: ( X = dom f & ( for x being Element of D st x in X holds
( H # x is convergent & lim (H # x) = f . x ) ) )
thus  X = dom f by A2; ::_thesis: for x being Element of D st x in X holds
( H # x is convergent & lim (H # x) = f . x )
let x be Element of D; ::_thesis: ( x in X implies ( H # x is convergent & lim (H # x) = f . x ) )
assume A4: x in X ; ::_thesis: ( H # x is convergent & lim (H # x) = f . x )
A5: now__::_thesis:_for_p_being_real_number_st_p_>_0_holds_
ex_k_being_Element_of_NAT_st_
for_n_being_Element_of_NAT_st_n_>=_k_holds_
abs_(((H_#_x)_._n)_-_(f_._x))_<_p
let p be real number ; ::_thesis: ( p > 0 implies ex k being Element of NAT st
for n being Element of NAT st n >= k holds
abs (((H # x) . n) - (f . x)) < p )
assume A6: p > 0 ; ::_thesis: ex k being Element of NAT st
for n being Element of NAT st n >= k holds
abs (((H # x) . n) - (f . x)) < p
 p is Real by XREAL_0:def_1;
then consider k being Element of NAT  such that
A7: for n being Element of NAT st n >= k holds
abs (((H . n) . x) - (f . x)) < p by A3, A4, A6;
take k = k; ::_thesis: for n being Element of NAT st n >= k holds
abs (((H # x) . n) - (f . x)) < p
let n be Element of NAT ; ::_thesis: ( n >= k implies abs (((H # x) . n) - (f . x)) < p )
assume  n >= k ; ::_thesis: abs (((H # x) . n) - (f . x)) < p
then  abs (((H . n) . x) - (f . x)) < p by A7;
hence  abs (((H # x) . n) - (f . x)) < p by Def10; ::_thesis: verum
end;
hence  H # x is convergent by SEQ_2:def_6; ::_thesis: lim (H # x) = f . x
hence  lim (H # x) = f . x by A5, SEQ_2:def_7; ::_thesis: verum
end;
assume A8: X common_on_dom H ; ::_thesis: ( for f being PartFunc of D,REAL holds
( not X = dom f or ex x being Element of D st
( x in X & not ( H # x is convergent & lim (H # x) = f . x ) ) ) or H is_point_conv_on X )
given f being PartFunc of D,REAL such that A9: X = dom f and
A10: for x being Element of D st x in X holds
( H # x is convergent & lim (H # x) = f . x ) ; ::_thesis: H is_point_conv_on X
 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 Element of NAT st
for n being Element of NAT st n >= k holds
abs (((H . n) . x) - (f . x)) < p ) )
proof
take  f ; ::_thesis: ( 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 Element of NAT st
for n being Element of NAT st n >= k holds
abs (((H . n) . x) - (f . x)) < p ) )
thus  X = dom f by A9; ::_thesis: 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
let x be Element of D; ::_thesis: ( x in X implies 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 )
assume  x in X ; ::_thesis: 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
then A11: ( H # x is convergent & lim (H # x) = f . x ) by A10;
let p be Real; ::_thesis: ( p > 0 implies ex k being Element of NAT st
for n being Element of NAT st n >= k holds
abs (((H . n) . x) - (f . x)) < p )
assume  p > 0 ; ::_thesis: ex k being Element of NAT st
for n being Element of NAT st n >= k holds
abs (((H . n) . x) - (f . x)) < p
then consider k being Element of NAT  such that
A12: for n being Element of NAT st n >= k holds
abs (((H # x) . n) - (f . x)) < p by A11, SEQ_2:def_7;
take  k ; ::_thesis: for n being Element of NAT st n >= k holds
abs (((H . n) . x) - (f . x)) < p
let n be Element of NAT ; ::_thesis: ( n >= k implies abs (((H . n) . x) - (f . x)) < p )
assume  n >= k ; ::_thesis: abs (((H . n) . x) - (f . x)) < p
then  abs (((H # x) . n) - (f . x)) < p by A12;
hence  abs (((H . n) . x) - (f . x)) < p by Def10; ::_thesis: verum
end;
hence  H is_point_conv_on X by A8, Def11; ::_thesis: verum
end;

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 & ( for x being Element of D st x in X holds
H # x is convergent ) ) )
proof
let D be non empty set ; ::_thesis: 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 ) ) )
let H be Functional_Sequence of D,REAL; ::_thesis: 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 ) ) )
let X be set ; ::_thesis: ( 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 ) ) )
defpred S1[ set ] means $1 in X;
deffunc H1( Element of D) ->  Element of REAL = lim (H # $1);
consider f being PartFunc of D,REAL such that
A1: for x being Element of D holds
( x in dom f iff S1[x] ) and
A2: for x being Element of D st x in dom f holds
f . x = H1(x) from SEQ_1:sch_3();
thus  ( H is_point_conv_on X implies ( X common_on_dom H & ( for x being Element of D st x in X holds
H # x is convergent ) ) ) ::_thesis: ( X common_on_dom H & ( for x being Element of D st x in X holds
H # x is convergent ) implies H is_point_conv_on X )
proof
assume A3: H is_point_conv_on X ; ::_thesis: ( X common_on_dom H & ( for x being Element of D st x in X holds
H # x is convergent ) )
hence  X common_on_dom H by Def11; ::_thesis: for x being Element of D st x in X holds
H # x is convergent
let x be Element of D; ::_thesis: ( x in X implies H # x is convergent )
assume A4: x in X ; ::_thesis: H # x is convergent
 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 ) ) ) by A3, Th19;
hence  H # x is convergent by A4; ::_thesis: verum
end;
assume that
A5: X common_on_dom H and
A6: for x being Element of D st x in X holds
H # x is convergent ; ::_thesis: H is_point_conv_on X
now__::_thesis:_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_&_f_._x_=_lim_(H_#_x)_)_)_)
take f = f; ::_thesis: ( X = dom f & ( for x being Element of D st x in X holds
( H # x is convergent & f . x = lim (H # x) ) ) )
thus A7: X = dom f ::_thesis: for x being Element of D st x in X holds
( H # x is convergent & f . x = lim (H # x) )
proof
thus  X c= dom f :: according to XBOOLE_0:def_10 ::_thesis: dom f c= X
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in X or x in dom f )
assume A8: x in X ; ::_thesis: x in dom f
 X c= dom (H . 0) by A5, Def9;
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  x in dom f ; ::_thesis: verum
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in dom f or x in X )
assume  x in dom f ; ::_thesis: x in X
hence  x in X by A1; ::_thesis: verum
end;
let x be Element of D; ::_thesis: ( x in X implies ( H # x is convergent & f . x = lim (H # x) ) )
assume A9: x in X ; ::_thesis: ( H # x is convergent & f . x = lim (H # x) )
hence  H # x is convergent by A6; ::_thesis: f . x = lim (H # x)
thus  f . x = lim (H # x) by A2, A7, A9; ::_thesis: verum
end;
hence  H is_point_conv_on X by A5, Th19; ::_thesis: verum
end;

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 & ex f being PartFunc of D,REAL st
( X = dom f & ( 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 & 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 & ex f being PartFunc of D,REAL st
( X = dom f & ( 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 & 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 & ( 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
consider f being PartFunc of D,REAL such that
A2: X = dom f and
A3: for x being Element of D st x in X holds
( H # x is convergent & lim (H # x) = f . x ) by A1, Th19;
take  f ; ::_thesis: ( dom f = X & ( for x being Element of D st x in dom f holds
f . x = lim (H # x) ) )
thus  dom f = X by A2; ::_thesis: for x being Element of D st x in dom f holds
f . x = lim (H # x)
let x be Element of D; ::_thesis: ( x in dom f implies f . x = lim (H # x) )
assume  x in dom f ; ::_thesis: f . x = lim (H # x)
hence  f . x = lim (H # x) by A2, A3; ::_thesis: verum
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
deffunc H1( Element of D) ->  Element of REAL = lim (H # $1);
thus  for f1, f2 being PartFunc of D,REAL st dom f1 = X & ( for x being Element of D st x in dom f1 holds
f1 . x = H1(x) ) & dom f2 = X & ( for x being Element of D st x in dom f2 holds
f2 . x = H1(x) ) holds
f1 = f2 from SEQ_1:sch_4(); ::_thesis: verum
end;
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 & ( 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 & ( 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 ) ) )
proof
let D be non empty set ; ::_thesis: 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 Element of NAT st
for n being Element of NAT st n >= k holds
abs (((H . n) . x) - (f . x)) < p ) ) )
let H be Functional_Sequence of D,REAL; ::_thesis: 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 Element of NAT st
for n being Element of NAT st n >= k holds
abs (((H . n) . x) - (f . x)) < p ) ) )
let X be set ; ::_thesis: 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 Element of NAT st
for n being Element of NAT st n >= k holds
abs (((H . n) . x) - (f . x)) < p ) ) )
let f be PartFunc of D,REAL; ::_thesis: ( H is_point_conv_on X implies ( 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 Element of NAT st
for n being Element of NAT st n >= k holds
abs (((H . n) . x) - (f . x)) < p ) ) ) )
assume A1: H is_point_conv_on X ; ::_thesis: ( 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 Element of NAT st
for n being Element of NAT st n >= k holds
abs (((H . n) . x) - (f . x)) < p ) ) )
thus  ( f = lim (H,X) implies ( 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 Element of NAT st
for n being Element of NAT st n >= k holds
abs (((H . n) . x) - (f . x)) < p ) ) ) ::_thesis: ( 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 Element of NAT st
for n being Element of NAT st n >= k holds
abs (((H . n) . x) - (f . x)) < p ) implies f = lim (H,X) )
proof
assume A2: f = lim (H,X) ; ::_thesis: ( 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 Element of NAT st
for n being Element of NAT st n >= k holds
abs (((H . n) . x) - (f . x)) < p ) )
hence A3: dom f = X by A1, Def13; ::_thesis: 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
let x be Element of D; ::_thesis: ( x in X implies 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 )
assume A4: x in X ; ::_thesis: 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
then A5: H # x is convergent by A1, Th20;
let p be Real; ::_thesis: ( p > 0 implies ex k being Element of NAT st
for n being Element of NAT st n >= k holds
abs (((H . n) . x) - (f . x)) < p )
assume A6: p > 0 ; ::_thesis: ex k being Element of NAT st
for n being Element of NAT st n >= k holds
abs (((H . n) . x) - (f . x)) < p
 f . x = lim (H # x) by A1, A2, A3, A4, Def13;
then consider k being Element of NAT  such that
A7: for n being Element of NAT st n >= k holds
abs (((H # x) . n) - (f . x)) < p by A5, A6, SEQ_2:def_7;
take  k ; ::_thesis: for n being Element of NAT st n >= k holds
abs (((H . n) . x) - (f . x)) < p
let n be Element of NAT ; ::_thesis: ( n >= k implies abs (((H . n) . x) - (f . x)) < p )
assume  n >= k ; ::_thesis: abs (((H . n) . x) - (f . x)) < p
then  abs (((H # x) . n) - (f . x)) < p by A7;
hence  abs (((H . n) . x) - (f . x)) < p by Def10; ::_thesis: verum
end;
assume that
A8: dom f = X and
A9: 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 ; ::_thesis: f = lim (H,X)
now__::_thesis:_for_x_being_Element_of_D_st_x_in_dom_f_holds_
f_._x_=_lim_(H_#_x)
let x be Element of D; ::_thesis: ( x in dom f implies f . x = lim (H # x) )
assume A10: x in dom f ; ::_thesis: f . x = lim (H # x)
A11: now__::_thesis:_for_p_being_real_number_st_p_>_0_holds_
ex_k_being_Element_of_NAT_st_
for_n_being_Element_of_NAT_st_n_>=_k_holds_
abs_(((H_#_x)_._n)_-_(f_._x))_<_p
let p be real number ; ::_thesis: ( p > 0 implies ex k being Element of NAT st
for n being Element of NAT st n >= k holds
abs (((H # x) . n) - (f . x)) < p )
assume A12: p > 0 ; ::_thesis: ex k being Element of NAT st
for n being Element of NAT st n >= k holds
abs (((H # x) . n) - (f . x)) < p
 p is Real by XREAL_0:def_1;
then consider k being Element of NAT  such that
A13: for n being Element of NAT st n >= k holds
abs (((H . n) . x) - (f . x)) < p by A8, A9, A10, A12;
take k = k; ::_thesis: for n being Element of NAT st n >= k holds
abs (((H # x) . n) - (f . x)) < p
let n be Element of NAT ; ::_thesis: ( n >= k implies abs (((H # x) . n) - (f . x)) < p )
assume  n >= k ; ::_thesis: abs (((H # x) . n) - (f . x)) < p
then  abs (((H . n) . x) - (f . x)) < p by A13;
hence  abs (((H # x) . n) - (f . x)) < p by Def10; ::_thesis: verum
end;
then  H # x is convergent by SEQ_2:def_6;
hence  f . x = lim (H # x) by A11, SEQ_2:def_7; ::_thesis: verum
end;
hence  f = lim (H,X) by A1, A8, Def13; ::_thesis: verum
end;

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
proof
let D be non empty set ; ::_thesis: 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
let H be Functional_Sequence of D,REAL; ::_thesis: for X being set st H is_unif_conv_on X holds
H is_point_conv_on X
let X be set ; ::_thesis: ( H is_unif_conv_on X implies H is_point_conv_on X )
assume A1: H is_unif_conv_on X ; ::_thesis: H is_point_conv_on X
A2: now__::_thesis:_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_Element_of_NAT_st_
for_n_being_Element_of_NAT_st_n_>=_k_holds_
abs_(((H_._n)_._x)_-_(f_._x))_<_p_)_)
consider f being PartFunc of D,REAL such that
A3: X = dom f and
A4: 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 & x in X holds
abs (((H . n) . x) - (f . x)) < p by A1, Def12;
take f = f; ::_thesis: ( 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 Element of NAT st
for n being Element of NAT st n >= k holds
abs (((H . n) . x) - (f . x)) < p ) )
thus  X = dom f by A3; ::_thesis: 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
let x be Element of D; ::_thesis: ( x in X implies 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 )
assume A5: x in X ; ::_thesis: 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
let p be Real; ::_thesis: ( p > 0 implies ex k being Element of NAT st
for n being Element of NAT st n >= k holds
abs (((H . n) . x) - (f . x)) < p )
assume  p > 0 ; ::_thesis: ex k being Element of NAT st
for n being Element of NAT st n >= k holds
abs (((H . n) . x) - (f . x)) < p
then consider k being Element of NAT  such that
A6: for n being Element of NAT
for x being Element of D st n >= k & x in X holds
abs (((H . n) . x) - (f . x)) < p by A4;
take k = k; ::_thesis: for n being Element of NAT st n >= k holds
abs (((H . n) . x) - (f . x)) < p
let n be Element of NAT ; ::_thesis: ( n >= k implies abs (((H . n) . x) - (f . x)) < p )
assume  n >= k ; ::_thesis: abs (((H . n) . x) - (f . x)) < p
hence  abs (((H . n) . x) - (f . x)) < p by A5, A6; ::_thesis: verum
end;
 X common_on_dom H by A1, Def12;
hence  H is_point_conv_on X by A2, Def11; ::_thesis: verum
end;

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 & Y <> {} & X common_on_dom H holds
Y common_on_dom H
proof
let D be non empty set ; ::_thesis: 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
let H be Functional_Sequence of D,REAL; ::_thesis: for Y, X being set st Y c= X & Y <> {} & X common_on_dom H holds
Y common_on_dom H
let Y, X be set ; ::_thesis: ( Y c= X & Y <> {} & X common_on_dom H implies Y common_on_dom H )
assume that
A1: Y c= X and
A2: Y <> {} and
A3: X common_on_dom H ; ::_thesis: Y common_on_dom H
now__::_thesis:_for_n_being_Element_of_NAT_holds_Y_c=_dom_(H_._n)
let n be Element of NAT ; ::_thesis: Y c= dom (H . n)
 X c= dom (H . n) by A3, Def9;
hence  Y c= dom (H . n) by A1, XBOOLE_1:1; ::_thesis: verum
end;
hence  Y common_on_dom H by A2, Def9; ::_thesis: verum
end;

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 & Y <> {} & H is_point_conv_on X holds
( H is_point_conv_on Y & (lim (H,X)) | Y = lim (H,Y) )
proof
let D be non empty set ; ::_thesis: 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) )
let H be Functional_Sequence of D,REAL; ::_thesis: 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) )
let Y, X be set ; ::_thesis: ( Y c= X & Y <> {} & H is_point_conv_on X implies ( H is_point_conv_on Y & (lim (H,X)) | Y = lim (H,Y) ) )
assume that
A1: Y c= X and
A2: Y <> {} and
A3: H is_point_conv_on X ; ::_thesis: ( H is_point_conv_on Y & (lim (H,X)) | Y = lim (H,Y) )
consider f being PartFunc of D,REAL such that
A4: X = dom f and
A5: 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 by A3, Def11;
A6: now__::_thesis:_ex_g_being_Element_of_K19(K20(D,REAL))_st_
(_Y_=_dom_g_&_(_for_x_being_Element_of_D_st_x_in_Y_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)_-_(g_._x))_<_p_)_)
take g = f | Y; ::_thesis: ( Y = dom g & ( for x being Element of D st x in Y 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) - (g . x)) < p ) )
thus A7: Y = dom g by A1, A4, RELAT_1:62; ::_thesis: for x being Element of D st x in Y 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) - (g . x)) < p
let x be Element of D; ::_thesis: ( x in Y implies 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) - (g . x)) < p )
assume A8: x in Y ; ::_thesis: 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) - (g . x)) < p
let p be Real; ::_thesis: ( p > 0 implies ex k being Element of NAT st
for n being Element of NAT st n >= k holds
abs (((H . n) . x) - (g . x)) < p )
assume  p > 0 ; ::_thesis: ex k being Element of NAT st
for n being Element of NAT st n >= k holds
abs (((H . n) . x) - (g . x)) < p
then consider k being Element of NAT  such that
A9: for n being Element of NAT st n >= k holds
abs (((H . n) . x) - (f . x)) < p by A1, A5, A8;
take k = k; ::_thesis: for n being Element of NAT st n >= k holds
abs (((H . n) . x) - (g . x)) < p
let n be Element of NAT ; ::_thesis: ( n >= k implies abs (((H . n) . x) - (g . x)) < p )
assume  n >= k ; ::_thesis: abs (((H . n) . x) - (g . x)) < p
then  abs (((H . n) . x) - (f . x)) < p by A9;
hence  abs (((H . n) . x) - (g . x)) < p by A7, A8, FUNCT_1:47; ::_thesis: verum
end;
 X common_on_dom H by A3, Def11;
then  Y common_on_dom H by A1, A2, Th23;
hence A10: H is_point_conv_on Y by A6, Def11; ::_thesis: (lim (H,X)) | Y = lim (H,Y)
A11: now__::_thesis:_for_x_being_Element_of_D_st_x_in_dom_((lim_(H,X))_|_Y)_holds_
((lim_(H,X))_|_Y)_._x_=_(lim_(H,Y))_._x
let x be Element of D; ::_thesis: ( x in dom ((lim (H,X)) | Y) implies ((lim (H,X)) | Y) . x = (lim (H,Y)) . x )
assume A12: x in dom ((lim (H,X)) | Y) ; ::_thesis: ((lim (H,X)) | Y) . x = (lim (H,Y)) . x
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 ; ::_thesis: verum
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  (lim (H,X)) | Y = lim (H,Y) by A11, PARTFUN1:5; ::_thesis: verum
end;

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 & Y <> {} & H is_unif_conv_on X holds
H is_unif_conv_on Y
proof
let D be non empty set ; ::_thesis: 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
let H be Functional_Sequence of D,REAL; ::_thesis: for Y, X being set st Y c= X & Y <> {} & H is_unif_conv_on X holds
H is_unif_conv_on Y
let Y, X be set ; ::_thesis: ( Y c= X & Y <> {} & H is_unif_conv_on X implies H is_unif_conv_on Y )
assume that
A1: Y c= X and
A2: Y <> {} and
A3: H is_unif_conv_on X ; ::_thesis: H is_unif_conv_on Y
consider f being PartFunc of D,REAL such that
A4: dom f = X and
A5: 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 & x in X holds
abs (((H . n) . x) - (f . x)) < p by A3, Def12;
A6: now__::_thesis:_ex_g_being_Element_of_K19(K20(D,REAL))_st_
(_dom_g_=_Y_&_(_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_&_x_in_Y_holds_
abs_(((H_._n)_._x)_-_(g_._x))_<_p_)_)
take g = f | Y; ::_thesis: ( dom g = Y & ( 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 & x in Y holds
abs (((H . n) . x) - (g . x)) < p ) )
thus A7: dom g = (dom f) /\ Y by RELAT_1:61
.= Y by A1, A4, XBOOLE_1:28 ; ::_thesis: 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 & x in Y holds
abs (((H . n) . x) - (g . x)) < p
let p be Real; ::_thesis: ( p > 0 implies ex k being Element of NAT st
for n being Element of NAT
for x being Element of D st n >= k & x in Y holds
abs (((H . n) . x) - (g . x)) < p )
assume  p > 0 ; ::_thesis: ex k being Element of NAT st
for n being Element of NAT
for x being Element of D st n >= k & x in Y holds
abs (((H . n) . x) - (g . x)) < p
then consider k being Element of NAT  such that
A8: for n being Element of NAT
for x being Element of D st n >= k & x in X holds
abs (((H . n) . x) - (f . x)) < p by A5;
take k = k; ::_thesis: for n being Element of NAT
for x being Element of D st n >= k & x in Y holds
abs (((H . n) . x) - (g . x)) < p
let n be Element of NAT ; ::_thesis: for x being Element of D st n >= k & x in Y holds
abs (((H . n) . x) - (g . x)) < p
let x be Element of D; ::_thesis: ( n >= k & x in Y implies abs (((H . n) . x) - (g . x)) < p )
assume that
A9: n >= k and
A10: x in Y ; ::_thesis: abs (((H . n) . x) - (g . x)) < p
 abs (((H . n) . x) - (f . x)) < p by A1, A8, A9, A10;
hence  abs (((H . n) . x) - (g . x)) < p by A7, A10, FUNCT_1:47; ::_thesis: verum
end;
 X common_on_dom H by A3, Def12;
then  Y common_on_dom H by A1, A2, Th23;
hence  H is_unif_conv_on Y by A6, Def12; ::_thesis: verum
end;

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
proof
let D be non empty set ; ::_thesis: 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
let H be Functional_Sequence of D,REAL; ::_thesis: 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
let X be set ; ::_thesis: ( X common_on_dom H implies for x being Element of D st x in X holds
{x} common_on_dom H )
assume A1: X common_on_dom H ; ::_thesis: for x being Element of D st x in X holds
{x} common_on_dom H
let x be Element of D; ::_thesis: ( x in X implies {x} common_on_dom H )
assume A2: x in X ; ::_thesis: {x} common_on_dom H
thus  {x} <> {} ; :: according to SEQFUNC:def_9 ::_thesis: for n being Element of NAT holds {x} c= dom (H . n)
now__::_thesis:_for_n_being_Element_of_NAT_holds_{x}_c=_dom_(H_._n)
let n be Element of NAT ; ::_thesis: {x} c= dom (H . n)
 X c= dom (H . n) by A1, Def9;
hence  {x} c= dom (H . n) by A2, ZFMISC_1:31; ::_thesis: verum
end;
hence  for n being Element of NAT holds {x} c= dom (H . n) ; ::_thesis: verum
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
proof
let D be non empty set ; ::_thesis: 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
let H be Functional_Sequence of D,REAL; ::_thesis: 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
let X be set ; ::_thesis: ( H is_point_conv_on X implies for x being Element of D st x in X holds
{x} common_on_dom H )
assume  H is_point_conv_on X ; ::_thesis: for x being Element of D st x in X holds
{x} common_on_dom H
then  X common_on_dom H by Def11;
hence  for x being Element of D st x in X holds
{x} common_on_dom H by Th26; ::_thesis: verum
end;

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 & {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
let D be non empty set ; ::_thesis: 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 )
let H1, H2 be Functional_Sequence of D,REAL; ::_thesis: 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 )
let x be Element of D; ::_thesis: ( {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 ) )
assume that
A1: {x} common_on_dom H1 and
A2: {x} common_on_dom H2 ; ::_thesis: ( (H1 # x) + (H2 # x) = (H1 + H2) # x & (H1 # x) - (H2 # x) = (H1 - H2) # x & (H1 # x) (#) (H2 # x) = (H1 (#) H2) # x )
now__::_thesis:_for_n_being_Element_of_NAT_holds_((H1_#_x)_+_(H2_#_x))_._n_=_((H1_+_H2)_#_x)_._n
let n be Element of NAT ; ::_thesis: ((H1 # x) + (H2 # x)) . n = ((H1 + H2) # x) . n
A3: {x} c= dom (H2 . n) by A2, Def9;
 ( x in {x} & {x} c= dom (H1 . n) ) by A1, Def9, 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 ; ::_thesis: verum
end;
hence  (H1 # x) + (H2 # x) = (H1 + H2) # x by FUNCT_2:63; ::_thesis: ( (H1 # x) - (H2 # x) = (H1 - H2) # x & (H1 # x) (#) (H2 # x) = (H1 (#) H2) # x )
now__::_thesis:_for_n_being_Element_of_NAT_holds_((H1_#_x)_-_(H2_#_x))_._n_=_((H1_-_H2)_#_x)_._n
let n be Element of NAT ; ::_thesis: ((H1 # x) - (H2 # x)) . n = ((H1 - H2) # x) . n
A5: {x} c= dom (H2 . n) by A2, Def9;
 ( x in {x} & {x} c= dom (H1 . n) ) by A1, Def9, 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 ; ::_thesis: verum
end;
hence  (H1 # x) - (H2 # x) = (H1 - H2) # x by FUNCT_2:63; ::_thesis: (H1 # x) (#) (H2 # x) = (H1 (#) H2) # x
now__::_thesis:_for_n_being_Element_of_NAT_holds_((H1_#_x)_(#)_(H2_#_x))_._n_=_((H1_(#)_H2)_#_x)_._n
let n be Element of NAT ; ::_thesis: ((H1 # x) (#) (H2 # x)) . n = ((H1 (#) H2) # x) . n
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 ; ::_thesis: verum
end;
hence  (H1 # x) (#) (H2 # x) = (H1 (#) H2) # x by FUNCT_2:63; ::_thesis: verum
end;

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) & (- H) # x = - (H # x) )
proof
let D be non empty set ; ::_thesis: 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) )
let H be Functional_Sequence of D,REAL; ::_thesis: for x being Element of D holds
( (abs H) # x = abs (H # x) & (- H) # x = - (H # x) )
let x be Element of D; ::_thesis: ( (abs H) # x = abs (H # x) & (- H) # x = - (H # x) )
now__::_thesis:_for_n_being_Element_of_NAT_holds_((abs_H)_#_x)_._n_=_(abs_(H_#_x))_._n
let n be Element of NAT ; ::_thesis: ((abs H) # x) . n = (abs (H # x)) . n
thus ((abs H) # x) . n = ((abs H) . n) . x by Def10
.= (abs (H . n)) . x by Def4
.= abs ((H . n) . x) by VALUED_1:18
.= abs ((H # x) . n) by Def10
.= (abs (H # x)) . n by SEQ_1:12 ; ::_thesis: verum
end;
hence  (abs H) # x = abs (H # x) by FUNCT_2:63; ::_thesis: (- H) # x = - (H # x)
now__::_thesis:_for_n_being_Element_of_NAT_holds_((-_H)_#_x)_._n_=_(-_(H_#_x))_._n
let n be Element of NAT ; ::_thesis: ((- H) # x) . n = (- (H # x)) . n
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 ; ::_thesis: verum
end;
hence  (- H) # x = - (H # x) by FUNCT_2:63; ::_thesis: verum
end;

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)
proof
let D be non empty set ; ::_thesis: 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)
let r be Real; ::_thesis: 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)
let H be Functional_Sequence of D,REAL; ::_thesis: for x being Element of D st {x} common_on_dom H holds
(r (#) H) # x = r (#) (H # x)
let x be Element of D; ::_thesis: ( {x} common_on_dom H implies (r (#) H) # x = r (#) (H # x) )
assume A1: {x} common_on_dom H ; ::_thesis: (r (#) H) # x = r (#) (H # x)
now__::_thesis:_for_n_being_Element_of_NAT_holds_((r_(#)_H)_#_x)_._n_=_(r_(#)_(H_#_x))_._n
let n be Element of NAT ; ::_thesis: ((r (#) H) # x) . n = (r (#) (H # x)) . n
 ( x in {x} & {x} c= dom (H . n) ) by A1, Def9, 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 ; ::_thesis: verum
end;
hence  (r (#) H) # x = r (#) (H # x) by FUNCT_2:63; ::_thesis: verum
end;

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 & 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
let D be non empty set ; ::_thesis: 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 )
let H1, H2 be Functional_Sequence of D,REAL; ::_thesis: 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 )
let X be set ; ::_thesis: ( X common_on_dom H1 & X common_on_dom H2 implies 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 ) )
assume A1: ( X common_on_dom H1 & X common_on_dom H2 ) ; ::_thesis: 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 )
let x be Element of D; ::_thesis: ( x in X implies ( (H1 # x) + (H2 # x) = (H1 + H2) # x & (H1 # x) - (H2 # x) = (H1 - H2) # x & (H1 # x) (#) (H2 # x) = (H1 (#) H2) # x ) )
assume  x in X ; ::_thesis: ( (H1 # x) + (H2 # x) = (H1 + H2) # x & (H1 # x) - (H2 # x) = (H1 - H2) # x & (H1 # x) (#) (H2 # x) = (H1 (#) H2) # x )
then  ( {x} common_on_dom H1 & {x} common_on_dom H2 ) by A1, Th26;
hence  ( (H1 # x) + (H2 # x) = (H1 + H2) # x & (H1 # x) - (H2 # x) = (H1 - H2) # x & (H1 # x) (#) (H2 # x) = (H1 (#) H2) # x ) by Th28; ::_thesis: verum
end;

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) & (- 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)
proof
let D be non empty set ; ::_thesis: 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)
let r be Real; ::_thesis: 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)
let H be Functional_Sequence of D,REAL; ::_thesis: 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)
let X be set ; ::_thesis: ( X common_on_dom H implies for x being Element of D st x in X holds
(r (#) H) # x = r (#) (H # x) )
assume A1: X common_on_dom H ; ::_thesis: for x being Element of D st x in X holds
(r (#) H) # x = r (#) (H # x)
let x be Element of D; ::_thesis: ( x in X implies (r (#) H) # x = r (#) (H # x) )
assume  x in X ; ::_thesis: (r (#) H) # x = r (#) (H # x)
then  {x} common_on_dom H by A1, Th26;
hence  (r (#) H) # x = r (#) (H # x) by Th30; ::_thesis: verum
end;

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 & 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
let D be non empty set ; ::_thesis: 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 )
let H1, H2 be Functional_Sequence of D,REAL; ::_thesis: 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 )
let X be set ; ::_thesis: ( H1 is_point_conv_on X & H2 is_point_conv_on X implies 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 ) )
assume  ( H1 is_point_conv_on X & H2 is_point_conv_on X ) ; ::_thesis: 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 )
then  ( X common_on_dom H1 & X common_on_dom H2 ) by Def11;
hence  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 Th31; ::_thesis: verum
end;

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) & (- 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)
proof
let D be non empty set ; ::_thesis: 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)
let r be Real; ::_thesis: 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)
let H be Functional_Sequence of D,REAL; ::_thesis: 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)
let X be set ; ::_thesis: ( H is_point_conv_on X implies for x being Element of D st x in X holds
(r (#) H) # x = r (#) (H # x) )
assume  H is_point_conv_on X ; ::_thesis: for x being Element of D st x in X holds
(r (#) H) # x = r (#) (H # x)
then  X common_on_dom H by Def11;
hence  for x being Element of D st x in X holds
(r (#) H) # x = r (#) (H # x) by Th33; ::_thesis: verum
end;

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 & 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
let D be non empty set ; ::_thesis: 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 )
let H1, H2 be Functional_Sequence of D,REAL; ::_thesis: 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 )
let X be set ; ::_thesis: ( 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 ) )
assume that
A1: X common_on_dom H1 and
A2: X common_on_dom H2 ; ::_thesis: ( X common_on_dom H1 + H2 & X common_on_dom H1 - H2 & X common_on_dom H1 (#) H2 )
A3: X <> {} by A1, Def9;
now__::_thesis:_for_n_being_Element_of_NAT_holds_X_c=_dom_((H1_+_H2)_._n)
let n be Element of NAT ; ::_thesis: X c= dom ((H1 + H2) . n)
 ( X c= dom (H1 . n) & X c= dom (H2 . n) ) by A1, A2, Def9;
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; ::_thesis: verum
end;
hence  X common_on_dom H1 + H2 by A3, Def9; ::_thesis: ( X common_on_dom H1 - H2 & X common_on_dom H1 (#) H2 )
now__::_thesis:_for_n_being_Element_of_NAT_holds_X_c=_dom_((H1_-_H2)_._n)
let n be Element of NAT ; ::_thesis: X c= dom ((H1 - H2) . n)
 ( X c= dom (H1 . n) & X c= dom (H2 . n) ) by A1, A2, Def9;
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; ::_thesis: verum
end;
hence  X common_on_dom H1 - H2 by A3, Def9; ::_thesis: X common_on_dom H1 (#) H2
now__::_thesis:_for_n_being_Element_of_NAT_holds_X_c=_dom_((H1_(#)_H2)_._n)
let n be Element of NAT ; ::_thesis: X c= dom ((H1 (#) H2) . n)
 ( X c= dom (H1 . n) & X c= dom (H2 . n) ) by A1, A2, Def9;
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; ::_thesis: verum
end;
hence  X common_on_dom H1 (#) H2 by A3, Def9; ::_thesis: verum
end;

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 & X common_on_dom - H )
proof
let D be non empty set ; ::_thesis: 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 )
let H be Functional_Sequence of D,REAL; ::_thesis: for X being set st X common_on_dom H holds
( X common_on_dom abs H & X common_on_dom - H )
let X be set ; ::_thesis: ( X common_on_dom H implies ( X common_on_dom abs H & X common_on_dom - H ) )
assume A1: X common_on_dom H ; ::_thesis: ( X common_on_dom abs H & X common_on_dom - H )
then A2: X <> {} by Def9;
now__::_thesis:_for_n_being_Element_of_NAT_holds_X_c=_dom_((abs_H)_._n)
let n be Element of NAT ; ::_thesis: X c= dom ((abs H) . n)
dom (H . n) = dom (abs (H . n)) by VALUED_1:def_11
.= dom ((abs H) . n) by Def4 ;
hence  X c= dom ((abs H) . n) by A1, Def9; ::_thesis: verum
end;
hence  X common_on_dom abs H by A2, Def9; ::_thesis: X common_on_dom - H
now__::_thesis:_for_n_being_Element_of_NAT_holds_X_c=_dom_((-_H)_._n)
let n be Element of NAT ; ::_thesis: X c= dom ((- H) . n)
dom (H . n) = dom (- (H . n)) by VALUED_1:8
.= dom ((- H) . n) by Def3 ;
hence  X c= dom ((- H) . n) by A1, Def9; ::_thesis: verum
end;
hence  X common_on_dom - H by A2, Def9; ::_thesis: verum
end;

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
proof
let D be non empty set ; ::_thesis: 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
let r be Real; ::_thesis: 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
let H be Functional_Sequence of D,REAL; ::_thesis: for X being set st X common_on_dom H holds
X common_on_dom r (#) H
let X be set ; ::_thesis: ( X common_on_dom H implies X common_on_dom r (#) H )
assume A1: X common_on_dom H ; ::_thesis: X common_on_dom r (#) H
A2: now__::_thesis:_for_n_being_Element_of_NAT_holds_X_c=_dom_((r_(#)_H)_._n)
let n be Element of NAT ; ::_thesis: X c= dom ((r (#) H) . 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, Def9; ::_thesis: verum
end;
 X <> {} by A1, Def9;
hence  X common_on_dom r (#) H by A2, Def9; ::_thesis: verum
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)) )
proof
let D be non empty set ; ::_thesis: 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)) )
let H1, H2 be Functional_Sequence of D,REAL; ::_thesis: 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)) )
let X be set ; ::_thesis: ( 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)) ) )
assume that
A1: H1 is_point_conv_on X and
A2: H2 is_point_conv_on X ; ::_thesis: ( 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)) )
A3: now__::_thesis:_for_x_being_Element_of_D_st_x_in_X_holds_
(H1_+_H2)_#_x_is_convergent
let x be Element of D; ::_thesis: ( x in X implies (H1 + H2) # x is convergent )
assume A4: x in X ; ::_thesis: (H1 + H2) # x is convergent
then  ( H1 # x is convergent & H2 # x is convergent ) by A1, A2, Th20;
then  (H1 # x) + (H2 # x) is convergent by SEQ_2:5;
hence  (H1 + H2) # x is convergent by A1, A2, A4, Th34; ::_thesis: verum
end;
A5: now__::_thesis:_for_x_being_Element_of_D_st_x_in_X_holds_
(H1_-_H2)_#_x_is_convergent
let x be Element of D; ::_thesis: ( x in X implies (H1 - H2) # x is convergent )
assume A6: x in X ; ::_thesis: (H1 - H2) # x is convergent
then  ( H1 # x is convergent & H2 # x is convergent ) by A1, A2, Th20;
then  (H1 # x) - (H2 # x) is convergent by SEQ_2:11;
hence  (H1 - H2) # x is convergent by A1, A2, A6, Th34; ::_thesis: verum
end;
A7: ( X common_on_dom H1 & X common_on_dom H2 ) by A1, A2, Th20;
then  X common_on_dom H1 + H2 by Th37;
hence A8: H1 + H2 is_point_conv_on X by A3, Th20; ::_thesis: ( 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)) )
A9: now__::_thesis:_for_x_being_Element_of_D_st_x_in_dom_((lim_(H1,X))_+_(lim_(H2,X)))_holds_
((lim_(H1,X))_+_(lim_(H2,X)))_._x_=_lim_((H1_+_H2)_#_x)
let x be Element of D; ::_thesis: ( x in dom ((lim (H1,X)) + (lim (H2,X))) implies ((lim (H1,X)) + (lim (H2,X))) . x = lim ((H1 + H2) # x) )
assume A10: x in dom ((lim (H1,X)) + (lim (H2,X))) ; ::_thesis: ((lim (H1,X)) + (lim (H2,X))) . x = lim ((H1 + 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, Th20;
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, Th34 ; ::_thesis: verum
end;
A16: now__::_thesis:_for_x_being_Element_of_D_st_x_in_X_holds_
(H1_(#)_H2)_#_x_is_convergent
let x be Element of D; ::_thesis: ( x in X implies (H1 (#) H2) # x is convergent )
assume A17: x in X ; ::_thesis: (H1 (#) H2) # x is convergent
then  ( H1 # x is convergent & H2 # x is convergent ) by A1, A2, Th20;
then  (H1 # x) (#) (H2 # x) is convergent by SEQ_2:14;
hence  (H1 (#) H2) # x is convergent by A1, A2, A17, Th34; ::_thesis: verum
end;
A18: now__::_thesis:_for_x_being_Element_of_D_st_x_in_dom_((lim_(H1,X))_(#)_(lim_(H2,X)))_holds_
((lim_(H1,X))_(#)_(lim_(H2,X)))_._x_=_lim_((H1_(#)_H2)_#_x)
let x be Element of D; ::_thesis: ( x in dom ((lim (H1,X)) (#) (lim (H2,X))) implies ((lim (H1,X)) (#) (lim (H2,X))) . x = lim ((H1 (#) H2) # x) )
assume  x in dom ((lim (H1,X)) (#) (lim (H2,X))) ; ::_thesis: ((lim (H1,X)) (#) (lim (H2,X))) . x = lim ((H1 (#) 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, Th20;
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, Th34 ; ::_thesis: verum
end;
A24: now__::_thesis:_for_x_being_Element_of_D_st_x_in_dom_((lim_(H1,X))_-_(lim_(H2,X)))_holds_
((lim_(H1,X))_-_(lim_(H2,X)))_._x_=_lim_((H1_-_H2)_#_x)
let x be Element of D; ::_thesis: ( x in dom ((lim (H1,X)) - (lim (H2,X))) implies ((lim (H1,X)) - (lim (H2,X))) . x = lim ((H1 - H2) # x) )
assume A25: x in dom ((lim (H1,X)) - (lim (H2,X))) ; ::_thesis: ((lim (H1,X)) - (lim (H2,X))) . x = lim ((H1 - 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, Th20;
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, Th34 ; ::_thesis: verum
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; ::_thesis: ( 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)) )
 X common_on_dom H1 - H2 by A7, Th37;
hence A31: H1 - H2 is_point_conv_on X by A5, Th20; ::_thesis: ( 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)) )
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; ::_thesis: ( H1 (#) H2 is_point_conv_on X & lim ((H1 (#) H2),X) = (lim (H1,X)) (#) (lim (H2,X)) )
 X common_on_dom H1 (#) H2 by A7, Th37;
hence A32: H1 (#) H2 is_point_conv_on X by A16, Th20; ::_thesis: lim ((H1 (#) H2),X) = (lim (H1,X)) (#) (lim (H2,X))
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  lim ((H1 (#) H2),X) = (lim (H1,X)) (#) (lim (H2,X)) by A32, A18, Def13; ::_thesis: verum
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) = abs (lim (H,X)) & - H is_point_conv_on X & lim ((- H),X) = - (lim (H,X)) )
proof
let D be non empty set ; ::_thesis: 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)) )
let H be Functional_Sequence of D,REAL; ::_thesis: 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)) )
let X be set ; ::_thesis: ( H is_point_conv_on X implies ( 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)) ) )
assume A1: H is_point_conv_on X ; ::_thesis: ( 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)) )
A2: now__::_thesis:_for_x_being_Element_of_D_st_x_in_X_holds_
(abs_H)_#_x_is_convergent
let x be Element of D; ::_thesis: ( x in X implies (abs H) # x is convergent )
assume  x in X ; ::_thesis: (abs H) # x is convergent
then  H # x is convergent by A1, Th20;
then  abs (H # x) is convergent by SEQ_4:13;
hence  (abs H) # x is convergent by Th32; ::_thesis: verum
end;
A3: now__::_thesis:_for_x_being_Element_of_D_st_x_in_dom_(-_(lim_(H,X)))_holds_
(-_(lim_(H,X)))_._x_=_lim_((-_H)_#_x)
let x be Element of D; ::_thesis: ( x in dom (- (lim (H,X))) implies (- (lim (H,X))) . x = lim ((- H) # x) )
assume  x in dom (- (lim (H,X))) ; ::_thesis: (- (lim (H,X))) . x = 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, Th20;
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 Th32 ; ::_thesis: verum
end;
A6: X common_on_dom H by A1, Th20;
then  X common_on_dom abs H by Th38;
hence A7: abs H is_point_conv_on X by A2, Th20; ::_thesis: ( lim ((abs H),X) = abs (lim (H,X)) & - H is_point_conv_on X & lim ((- H),X) = - (lim (H,X)) )
A8: now__::_thesis:_for_x_being_Element_of_D_st_x_in_dom_(abs_(lim_(H,X)))_holds_
(abs_(lim_(H,X)))_._x_=_lim_((abs_H)_#_x)
let x be Element of D; ::_thesis: ( x in dom (abs (lim (H,X))) implies (abs (lim (H,X))) . x = lim ((abs H) # x) )
assume  x in dom (abs (lim (H,X))) ; ::_thesis: (abs (lim (H,X))) . x = lim ((abs 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, Th20;
thus (abs (lim (H,X))) . x = abs ((lim (H,X)) . x) by VALUED_1:18
.= abs (lim (H # x)) by A1, A9, Def13
.= lim (abs (H # x)) by A10, SEQ_4:14
.= lim ((abs H) # x) by Th32 ; ::_thesis: verum
end;
A11: now__::_thesis:_for_x_being_Element_of_D_st_x_in_X_holds_
(-_H)_#_x_is_convergent
let x be Element of D; ::_thesis: ( x in X implies (- H) # x is convergent )
assume  x in X ; ::_thesis: (- H) # x is convergent
then  H # x is convergent by A1, Th20;
then  - (H # x) is convergent by SEQ_2:9;
hence  (- H) # x is convergent by Th32; ::_thesis: verum
end;
dom (abs (lim (H,X))) = dom (lim (H,X)) by VALUED_1:def_11
.= X by A1, Def13 ;
hence  lim ((abs H),X) = abs (lim (H,X)) by A7, A8, Def13; ::_thesis: ( - H is_point_conv_on X & lim ((- H),X) = - (lim (H,X)) )
 X common_on_dom - H by A6, Th38;
hence A12: - H is_point_conv_on X by A11, Th20; ::_thesis: lim ((- H),X) = - (lim (H,X))
dom (- (lim (H,X))) = dom (lim (H,X)) by VALUED_1:8
.= X by A1, Def13 ;
hence  lim ((- H),X) = - (lim (H,X)) by A12, A3, Def13; ::_thesis: verum
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)) )
proof
let D be non empty set ; ::_thesis: 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)) )
let r be Real; ::_thesis: 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)) )
let H be Functional_Sequence of D,REAL; ::_thesis: 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)) )
let X be set ; ::_thesis: ( H is_point_conv_on X implies ( r (#) H is_point_conv_on X & lim ((r (#) H),X) = r (#) (lim (H,X)) ) )
assume A1: H is_point_conv_on X ; ::_thesis: ( r (#) H is_point_conv_on X & lim ((r (#) H),X) = r (#) (lim (H,X)) )
then A2: X common_on_dom H by Th20;
A3: now__::_thesis:_for_x_being_Element_of_D_st_x_in_dom_(r_(#)_(lim_(H,X)))_holds_
(r_(#)_(lim_(H,X)))_._x_=_lim_((r_(#)_H)_#_x)
let x be Element of D; ::_thesis: ( x in dom (r (#) (lim (H,X))) implies (r (#) (lim (H,X))) . x = lim ((r (#) H) # x) )
assume A4: x in dom (r (#) (lim (H,X))) ; ::_thesis: (r (#) (lim (H,X))) . x = lim ((r (#) 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, Th20;
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, Th33 ; ::_thesis: verum
end;
A8: now__::_thesis:_for_x_being_Element_of_D_st_x_in_X_holds_
(r_(#)_H)_#_x_is_convergent
let x be Element of D; ::_thesis: ( x in X implies (r (#) H) # x is convergent )
assume A9: x in X ; ::_thesis: (r (#) H) # x is convergent
then  H # x is convergent by A1, Th20;
then  r (#) (H # x) is convergent by SEQ_2:7;
hence  (r (#) H) # x is convergent by A2, A9, Th33; ::_thesis: verum
end;
 X common_on_dom r (#) H by A2, Th39;
hence A10: r (#) H is_point_conv_on X by A8, Th20; ::_thesis: lim ((r (#) H),X) = r (#) (lim (H,X))
dom (r (#) (lim (H,X))) = dom (lim (H,X)) by VALUED_1:def_5
.= X by A1, Def13 ;
hence  lim ((r (#) H),X) = r (#) (lim (H,X)) by A10, A3, Def13; ::_thesis: verum
end;

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 & H is_point_conv_on X & ( 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 & x in X holds
abs (((H . n) . x) - ((lim (H,X)) . x)) < r ) ) )
proof
let D be non empty set ; ::_thesis: 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 Element of NAT st
for n being Element of NAT
for x being Element of D st n >= k & x in X holds
abs (((H . n) . x) - ((lim (H,X)) . x)) < r ) ) )
let H be Functional_Sequence of D,REAL; ::_thesis: 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 Element of NAT st
for n being Element of NAT
for x being Element of D st n >= k & x in X holds
abs (((H . n) . x) - ((lim (H,X)) . x)) < r ) ) )
let X be set ; ::_thesis: ( 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 Element of NAT st
for n being Element of NAT
for x being Element of D st n >= k & x in X holds
abs (((H . n) . x) - ((lim (H,X)) . x)) < r ) ) )
thus  ( H is_unif_conv_on X implies ( X common_on_dom H & H is_point_conv_on X & ( 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 & x in X holds
abs (((H . n) . x) - ((lim (H,X)) . x)) < r ) ) ) ::_thesis: ( X common_on_dom H & H is_point_conv_on X & ( 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 & x in X holds
abs (((H . n) . x) - ((lim (H,X)) . x)) < r ) implies H is_unif_conv_on X )
proof
assume A1: H is_unif_conv_on X ; ::_thesis: ( X common_on_dom H & H is_point_conv_on X & ( 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 & x in X holds
abs (((H . n) . x) - ((lim (H,X)) . x)) < r ) )
then consider f being PartFunc of D,REAL such that
A2: X = dom f and
A3: 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 & x in X holds
abs (((H . n) . x) - (f . x)) < p by Def12;
thus  X common_on_dom H by A1, Def12; ::_thesis: ( H is_point_conv_on X & ( 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 & x in X holds
abs (((H . n) . x) - ((lim (H,X)) . x)) < r ) )
A4: now__::_thesis:_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
let x be Element of D; ::_thesis: ( x in X implies 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 )
assume A5: x in X ; ::_thesis: 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
let p be Real; ::_thesis: ( p > 0 implies ex k being Element of NAT st
for n being Element of NAT st n >= k holds
abs (((H . n) . x) - (f . x)) < p )
assume  p > 0 ; ::_thesis: ex k being Element of NAT st
for n being Element of NAT st n >= k holds
abs (((H . n) . x) - (f . x)) < p
then consider k being Element of NAT  such that
A6: for n being Element of NAT
for x being Element of D st n >= k & x in X holds
abs (((H . n) . x) - (f . x)) < p by A3;
take k = k; ::_thesis: for n being Element of NAT st n >= k holds
abs (((H . n) . x) - (f . x)) < p
let n be Element of NAT ; ::_thesis: ( n >= k implies abs (((H . n) . x) - (f . x)) < p )
assume  n >= k ; ::_thesis: abs (((H . n) . x) - (f . x)) < p
hence  abs (((H . n) . x) - (f . x)) < p by A5, A6; ::_thesis: verum
end;
thus  H is_point_conv_on X by A1, Th22; ::_thesis: 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 & x in X holds
abs (((H . n) . x) - ((lim (H,X)) . x)) < r
then A7: f = lim (H,X) by A2, A4, Th21;
let r be Real; ::_thesis: ( 0 < r implies ex k being Element of NAT st
for n being Element of NAT
for x being Element of D st n >= k & x in X holds
abs (((H . n) . x) - ((lim (H,X)) . x)) < r )
assume  r > 0 ; ::_thesis: ex k being Element of NAT st
for n being Element of NAT
for x being Element of D st n >= k & x in X holds
abs (((H . n) . x) - ((lim (H,X)) . x)) < r
then consider k being Element of NAT  such that
A8: for n being Element of NAT
for x being Element of D st n >= k & x in X holds
abs (((H . n) . x) - (f . x)) < r by A3;
take  k ; ::_thesis: for n being Element of NAT
for x being Element of D st n >= k & x in X holds
abs (((H . n) . x) - ((lim (H,X)) . x)) < r
let n be Element of NAT ; ::_thesis: for x being Element of D st n >= k & x in X holds
abs (((H . n) . x) - ((lim (H,X)) . x)) < r
let x be Element of D; ::_thesis: ( n >= k & x in X implies abs (((H . n) . x) - ((lim (H,X)) . x)) < r )
assume  ( n >= k & x in X ) ; ::_thesis: abs (((H . n) . x) - ((lim (H,X)) . x)) < r
hence  abs (((H . n) . x) - ((lim (H,X)) . x)) < r by A7, A8; ::_thesis: verum
end;
assume that
A9: X common_on_dom H and
A10: H is_point_conv_on X and
A11: 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 & x in X holds
abs (((H . n) . x) - ((lim (H,X)) . x)) < r ; ::_thesis: H is_unif_conv_on X
 dom (lim (H,X)) = X by A10, Def13;
hence  H is_unif_conv_on X by A9, A11, Def12; ::_thesis: verum
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 Element of NAT holds (H . n) | X is continuous ) holds
(lim (H,X)) | X is continuous
proof
let X be set ; ::_thesis: for H being Functional_Sequence of REAL,REAL st H is_unif_conv_on X & ( for n being Element of NAT holds (H . n) | X is continuous ) holds
(lim (H,X)) | X is continuous
let H be Functional_Sequence of REAL,REAL; ::_thesis: ( H is_unif_conv_on X & ( for n being Element of NAT holds (H . n) | X is continuous ) implies (lim (H,X)) | X is continuous )
set l = lim (H,X);
assume that
A1: H is_unif_conv_on X and
A2: for n being Element of NAT holds (H . n) | X is continuous ; ::_thesis: (lim (H,X)) | X is continuous
A3: H is_point_conv_on X by A1, Th22;
then A4: dom (lim (H,X)) = X by Def13;
A5: X common_on_dom H by A1, Def12;
 for x0 being real number st x0 in dom ((lim (H,X)) | X) holds
(lim (H,X)) | X is_continuous_in x0
proof
let x0 be real number ; ::_thesis: ( x0 in dom ((lim (H,X)) | X) implies (lim (H,X)) | X is_continuous_in x0 )
assume  x0 in dom ((lim (H,X)) | X) ; ::_thesis: (lim (H,X)) | X is_continuous_in x0
then A6: x0 in X by RELAT_1:57;
reconsider x0 = x0 as Real by XREAL_0:def_1;
 for r being real number st 0 < r holds
ex s being real number st
( 0 < s & ( for x1 being real number st x1 in dom ((lim (H,X)) | X) & abs (x1 - x0) < s holds
abs ((((lim (H,X)) | X) . x1) - (((lim (H,X)) | X) . x0)) < r ) )
proof
let r be real number ; ::_thesis: ( 0 < r implies ex s being real number st
( 0 < s & ( for x1 being real number st x1 in dom ((lim (H,X)) | X) & abs (x1 - x0) < s holds
abs ((((lim (H,X)) | X) . x1) - (((lim (H,X)) | X) . x0)) < r ) ) )
assume  0 < r ; ::_thesis: ex s being real number st
( 0 < s & ( for x1 being real number st x1 in dom ((lim (H,X)) | X) & abs (x1 - x0) < s holds
abs ((((lim (H,X)) | X) . x1) - (((lim (H,X)) | X) . x0)) < r ) )
then A7: 0 < r / 3 by XREAL_1:222;
reconsider r = r as Real by XREAL_0:def_1;
consider k being Element of NAT  such that
A8: for n being Element of NAT
for x1 being Real st n >= k & x1 in X holds
abs (((H . n) . x1) - ((lim (H,X)) . x1)) < r / 3 by A1, A7, Th43;
consider k1 being Element of NAT  such that
A9: for n being Element of NAT st n >= k1 holds
abs (((H . n) . x0) - ((lim (H,X)) . x0)) < r / 3 by A3, A6, A7, Th21;
set m = max (k,k1);
set h = H . (max (k,k1));
A10: X c= dom (H . (max (k,k1))) by A5, Def9;
A11: dom ((H . (max (k,k1))) | X) = (dom (H . (max (k,k1)))) /\ X by RELAT_1:61
.= X by A10, XBOOLE_1:28 ;
 (H . (max (k,k1))) | X is continuous by A2;
then  (H . (max (k,k1))) | X is_continuous_in x0 by A6, A11, FCONT_1:def_2;
then consider s being real number  such that
A12: 0 < s and
A13: for x1 being real number st x1 in dom ((H . (max (k,k1))) | X) & abs (x1 - x0) < s holds
abs ((((H . (max (k,k1))) | X) . x1) - (((H . (max (k,k1))) | X) . x0)) < r / 3 by A7, FCONT_1:3;
reconsider s = s as Real by XREAL_0:def_1;
take  s ; ::_thesis: ( 0 < s & ( for x1 being real number st x1 in dom ((lim (H,X)) | X) & abs (x1 - x0) < s holds
abs ((((lim (H,X)) | X) . x1) - (((lim (H,X)) | X) . x0)) < r ) )
thus  0 < s by A12; ::_thesis: for x1 being real number st x1 in dom ((lim (H,X)) | X) & abs (x1 - x0) < s holds
abs ((((lim (H,X)) | X) . x1) - (((lim (H,X)) | X) . x0)) < r
let x1 be real number ; ::_thesis: ( x1 in dom ((lim (H,X)) | X) & abs (x1 - x0) < s implies abs ((((lim (H,X)) | X) . x1) - (((lim (H,X)) | X) . x0)) < r )
assume that
A14: x1 in dom ((lim (H,X)) | X) and
A15: abs (x1 - x0) < s ; ::_thesis: abs ((((lim (H,X)) | X) . x1) - (((lim (H,X)) | X) . x0)) < r
A16: dom ((lim (H,X)) | X) = (dom (lim (H,X))) /\ X by RELAT_1:61
.= X by A4 ;
then  abs ((((H . (max (k,k1))) | X) . x1) - (((H . (max (k,k1))) | X) . x0)) < r / 3 by A11, A13, A14, A15;
then  abs (((H . (max (k,k1))) . x1) - (((H . (max (k,k1))) | X) . x0)) < r / 3 by A16, A11, A14, FUNCT_1:47;
then A17: abs (((H . (max (k,k1))) . x1) - ((H . (max (k,k1))) . x0)) < r / 3 by A6, FUNCT_1:49;
 abs (((H . (max (k,k1))) . x0) - ((lim (H,X)) . x0)) < r / 3 by A9, XXREAL_0:25;
then  ( abs ((((H . (max (k,k1))) . x1) - ((H . (max (k,k1))) . x0)) + (((H . (max (k,k1))) . x0) - ((lim (H,X)) . x0))) <= (abs (((H . (max (k,k1))) . x1) - ((H . (max (k,k1))) . x0))) + (abs (((H . (max (k,k1))) . x0) - ((lim (H,X)) . x0))) & (abs (((H . (max (k,k1))) . x1) - ((H . (max (k,k1))) . x0))) + (abs (((H . (max (k,k1))) . x0) - ((lim (H,X)) . x0))) < (r / 3) + (r / 3) ) by A17, COMPLEX1:56, XREAL_1:8;
then A18: abs ((((H . (max (k,k1))) . x1) - ((H . (max (k,k1))) . x0)) + (((H . (max (k,k1))) . x0) - ((lim (H,X)) . x0))) < (r / 3) + (r / 3) by XXREAL_0:2;
 abs (((lim (H,X)) . x1) - ((lim (H,X)) . x0)) = abs ((((lim (H,X)) . x1) - ((H . (max (k,k1))) . x1)) + ((((H . (max (k,k1))) . x1) - ((H . (max (k,k1))) . x0)) + (((H . (max (k,k1))) . x0) - ((lim (H,X)) . x0)))) ;
then A19: abs (((lim (H,X)) . x1) - ((lim (H,X)) . x0)) <= (abs (((lim (H,X)) . x1) - ((H . (max (k,k1))) . x1))) + (abs ((((H . (max (k,k1))) . x1) - ((H . (max (k,k1))) . x0)) + (((H . (max (k,k1))) . x0) - ((lim (H,X)) . x0)))) by COMPLEX1:56;
 abs (((H . (max (k,k1))) . x1) - ((lim (H,X)) . x1)) < r / 3 by A8, A16, A14, XXREAL_0:25;
then  abs (- (((lim (H,X)) . x1) - ((H . (max (k,k1))) . x1))) < r / 3 ;
then  abs (((lim (H,X)) . x1) - ((H . (max (k,k1))) . x1)) < r / 3 by COMPLEX1:52;
then  (abs (((lim (H,X)) . x1) - ((H . (max (k,k1))) . x1))) + (abs ((((H . (max (k,k1))) . x1) - ((H . (max (k,k1))) . x0)) + (((H . (max (k,k1))) . x0) - ((lim (H,X)) . x0)))) < (r / 3) + ((r / 3) + (r / 3)) by A18, XREAL_1:8;
then  abs (((lim (H,X)) . x1) - ((lim (H,X)) . x0)) < ((r / 3) + (r / 3)) + (r / 3) by A19, XXREAL_0:2;
then  abs ((((lim (H,X)) | X) . x1) - ((lim (H,X)) . x0)) < r by A14, FUNCT_1:47;
hence  abs ((((lim (H,X)) | X) . x1) - (((lim (H,X)) | X) . x0)) < r by A4, RELAT_1:68; ::_thesis: verum
end;
hence  (lim (H,X)) | X is_continuous_in x0 by FCONT_1:3; ::_thesis: verum
end;
hence  (lim (H,X)) | X is continuous by FCONT_1:def_2; ::_thesis: verum
end;