end;

then BoundedFunctions ( the carrier of S,T) c= PFuncs ( the carrier of S, the carrier of T) ;
then reconsider H = seq as Functional_Sequence of the carrier of S, the carrier of T by FUNCT_2:7;
A4: for n being Nat holds the carrier of S c= dom (H . n)

let n be Nat; :: thesis:
H . n in rng seq by ORDINAL1:def 12, FUNCT_2:4;
then H . n in Y by A2;
then consider f being Function of the carrier of S, the carrier of T such that
A5: ( H . n = f & f is continuous ) by A1;
thus the carrier of S c= dom (H . n) by A5, FUNCT_2:def 1; :: thesis:

end;

A6: for p being Real st p > 0 holds
ex k being Nat st
for n being Nat
for x being Element of the carrier of S st n >= k & x in the carrier of S holds
||.(((H . n) /. x) - (f /. x)).|| < p

let p be Real; :: thesis:
assume p > 0 ; :: thesis:
then consider k being Nat such that
A7: for n being Nat st n >= k holds
||.((seq . n) - (lim seq)).|| < p by A2, NORMSP_1:def 7;
reconsider k = k as Element of NAT by ORDINAL1:def 12;
take k ; :: thesis:

let n be Nat; :: thesis:
let x be Element of S; :: thesis:
assume ( n >= k & x in the carrier of S ) ; :: thesis:
then A8: ||.((seq . n) - (lim seq)).|| < p by A7;
reconsider g = (seq . n) - (lim seq) as bounded Function of the carrier of S, the carrier of T by RSSPACE4:def 5;
reconsider s = seq . n as bounded Function of the carrier of S, the carrier of T by RSSPACE4:def 5;
reconsider x0 = x as Element of the carrier of S ;
A9: g . x0 = (s . x0) - (f . x0) by RSSPACE4:24;
A10: ||.(g . x0).|| <= ||.((seq . n) - (lim seq)).|| by RSSPACE4:16;
H . n in rng seq by ORDINAL1:def 12, FUNCT_2:4;
then H . n in Y by A2;
then ex f being Function of the carrier of S, the carrier of T st
( H . n = f & f is continuous ) by A1;
then dom (H . n) = the carrier of S by FUNCT_2:def 1;
then (H . n) . x = (H . n) /. x by PARTFUN1:def 6;
hence ||.(((H . n) /. x) - (f /. x)).|| < p by A9, A10, A8, XXREAL_0:2; :: thesis:

end;

A12: for x being Element of the carrier of S st x in the carrier of S holds
for p being Real st p > 0 holds
ex k being Nat st
for n being Nat st n >= k holds
||.(((H . n) /. x) - (f /. x)).|| < p

let x be Element of the carrier of S; :: thesis:
assume x in the carrier of S ; :: thesis:
let p be Real; :: thesis:
assume p > 0 ; :: thesis:
then consider k being Nat such that
A13: for n being Nat
for x being Element of the carrier of S st n >= k & x in the carrier of S holds
||.(((H . n) /. x) - (f /. x)).|| < p by A6;
take k ; :: thesis:
let n be Nat; :: thesis:
assume n >= k ; :: thesis:
hence ||.(((H . n) /. x) - (f /. x)).|| < p by A13; :: thesis:

end;

let n be Nat; :: thesis:
H . n in rng seq by ORDINAL1:def 12, FUNCT_2:4;
then H . n in Y by A2;
then consider f being Function of the carrier of S, the carrier of T such that
A17: ( H . n = f & f is continuous ) by A1;
thus ex Hn being Function of S,T st
( Hn = H . n & Hn is continuous ) by A17; :: thesis:

end;

end;