let D be non empty set ; :: thesis: for Z being set
for Y being RealNormSpace
for H being Functional_Sequence of D, the carrier of Y
for X being set st Z c= X & Z <> {} & H is_unif_conv_on X holds
H is_unif_conv_on Z
let Z be set ; :: thesis: for Y being RealNormSpace
for H being Functional_Sequence of D, the carrier of Y
for X being set st Z c= X & Z <> {} & H is_unif_conv_on X holds
H is_unif_conv_on Z
let Y be RealNormSpace; :: thesis: for H being Functional_Sequence of D, the carrier of Y
for X being set st Z c= X & Z <> {} & H is_unif_conv_on X holds
H is_unif_conv_on Z
let H be Functional_Sequence of D, the carrier of Y; :: thesis: for X being set st Z c= X & Z <> {} & H is_unif_conv_on X holds
H is_unif_conv_on Z
let X be set ; :: thesis: ( Z c= X & Z <> {} & H is_unif_conv_on X implies H is_unif_conv_on Z )
assume that
A1: Z c= X and
A2: Z <> {} and
A3: H is_unif_conv_on X ; :: thesis: H is_unif_conv_on Z
consider f being PartFunc of D, the carrier of Y such that
A4: dom f = X and
A5: for p being Real st p > 0 holds
ex k being Nat st
for n being Nat
for x being Element of D st n >= k & x in X holds
||.(((H . n) /. x) - (f /. x)).|| < p by A3;

now :: thesis: ex g being Element of K16(K17(D, the carrier of Y)) st
( dom g = Z & ( for p being Real st p > 0 holds
ex k being Nat st
for n being Nat
for x being Element of D st n >= k & x in Z holds
||.(((H . n) /. x) - (g /. x)).|| < p ) )

take g = f | Z; :: thesis: ( dom g = Z & ( for p being Real st p > 0 holds
ex k being Nat st
for n being Nat
for x being Element of D st n >= k & x in Z holds
||.(((H . n) /. x) - (g /. x)).|| < p ) )
thus A7: dom g = (dom f) /\ Z by RELAT_1:61
.= Z by A1, A4, XBOOLE_1:28 ; :: thesis: for p being Real st p > 0 holds
ex k being Nat st
for n being Nat
for x being Element of D st n >= k & x in Z holds
||.(((H . n) /. x) - (g /. x)).|| < p
let p be Real; :: thesis: ( p > 0 implies ex k being Nat st
for n being Nat
for x being Element of D st n >= k & x in Z holds
||.(((H . n) /. x) - (g /. x)).|| < p )
assume p > 0 ; :: thesis: ex k being Nat st
for n being Nat
for x being Element of D st n >= k & x in Z holds
||.(((H . n) /. x) - (g /. x)).|| < p
then consider k being Nat such that
A8: for n being Nat
for x being Element of D st n >= k & x in X holds
||.(((H . n) /. x) - (f /. x)).|| < p by A5;
take k = k; :: thesis: for n being Nat
for x being Element of D st n >= k & x in Z holds
||.(((H . n) /. x) - (g /. x)).|| < p
let n be Nat; :: thesis: for x being Element of D st n >= k & x in Z holds
||.(((H . n) /. x) - (g /. x)).|| < p
let x be Element of D; :: thesis: ( n >= k & x in Z implies ||.(((H . n) /. x) - (g /. x)).|| < p )
assume that
A9: n >= k and
A10: x in Z ; :: thesis: ||.(((H . n) /. x) - (g /. x)).|| < p
( x in Z & x in dom f ) by A7, A10, RELAT_1:57;
then f /. x = f . x by PARTFUN1:def 6
.= g . x by A7, A10, FUNCT_1:47
.= g /. x by A10, A7, PARTFUN1:def 6 ;
hence ||.(((H . n) /. x) - (g /. x)).|| < p by A1, A8, A9, A10; :: thesis: verum

end;

hence H is_unif_conv_on Z by A1, A2, A3, Th22; :: thesis: verum