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, Def13;

A6: now

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:90
.= 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:70; :: thesis: verum

end;

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