let D be non empty set ; :: thesis: for H being Functional_Sequence of D,REAL
for X, Y 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 X, Y being set st Y c= X & Y <> {} & H is_unif_conv_on X holds
H is_unif_conv_on Y
let X, Y 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 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;

A6: now :: thesis: ex g being Element of bool [:D,REAL:] st
( dom g = Y & ( 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 Y holds
|.(((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 Nat st
for n being Nat
for x being Element of D st n >= k & x in Y holds
|.(((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 Nat st
for n being Nat
for x being Element of D st n >= k & x in Y 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 Y 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 Y 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 Y holds
|.(((H . n) . x) - (g . x)).| < p
let n be Nat; :: thesis: for x being Element of D st n >= k & x in Y holds
|.(((H . n) . x) - (g . x)).| < p
let x be Element of D; :: thesis: ( n >= k & x in Y implies |.(((H . n) . x) - (g . x)).| < p )
assume that
A9: n >= k and
A10: x in Y ; :: thesis: |.(((H . n) . x) - (g . x)).| < p
|.(((H . n) . x) - (f . x)).| < p by A1, A8, A9, A10;
hence |.(((H . n) . x) - (g . x)).| < p by A7, A10, FUNCT_1:47; :: thesis: verum

end;

X common_on_dom H by A3;
then Y common_on_dom H by A1, A2, Th22;
hence H is_unif_conv_on Y by A6; :: thesis: verum