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 A1: ( Y c= X & Y <> {} & H is_unif_conv_on X ) ; :: thesis: H is_unif_conv_on Y
then X common_on_dom H by Def13;
then A2: Y common_on_dom H by A1, Th24;
consider f being PartFunc of D, REAL such that
A3: ( dom f = X & ( 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, Def13;

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 A4: dom g = (dom f) /\ Y by RELAT_1:90
.= Y by A1, A3, 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
A5: 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
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 A6: ( n >= k & x in Y ) ; :: thesis: abs (((H . n) . x) - (g . x)) < p
then abs (((H . n) . x) - (f . x)) < p by A1, A5;
hence abs (((H . n) . x) - (g . x)) < p by A4, A6, FUNCT_1:68; :: thesis: verum

end;

hence H is_unif_conv_on Y by A2, Def13; :: thesis: verum