let CNS be ComplexNormSpace; for RNS being RealNormSpace
for X, X1 being set
for f being PartFunc of CNS,RNS st f is_continuous_on X & X1 c= X holds
f is_continuous_on X1
let RNS be RealNormSpace; for X, X1 being set
for f being PartFunc of CNS,RNS st f is_continuous_on X & X1 c= X holds
f is_continuous_on X1
let X, X1 be set ; for f being PartFunc of CNS,RNS st f is_continuous_on X & X1 c= X holds
f is_continuous_on X1
let f be PartFunc of CNS,RNS; ( f is_continuous_on X & X1 c= X implies f is_continuous_on X1 )
assume that
A1:
f is_continuous_on X
and
A2:
X1 c= X
; f is_continuous_on X1
X c= dom f
by A1;
hence A3:
X1 c= dom f
by A2; NCFCONT1:def 12 for x0 being Point of CNS st x0 in X1 holds
f | X1 is_continuous_in x0
let r be Point of CNS; ( r in X1 implies f | X1 is_continuous_in r )
assume A4:
r in X1
; f | X1 is_continuous_in r
then A5:
f | X is_continuous_in r
by A1, A2;
thus
f | X1 is_continuous_in r
verumproof
(dom f) /\ X1 c= (dom f) /\ X
by A2, XBOOLE_1:26;
then
dom (f | X1) c= (dom f) /\ X
by RELAT_1:61;
then A6:
dom (f | X1) c= dom (f | X)
by RELAT_1:61;
r in (dom f) /\ X1
by A3, A4, XBOOLE_0:def 4;
hence A7:
r in dom (f | X1)
by RELAT_1:61;
NCFCONT1:def 6 for seq being sequence of CNS st rng seq c= dom (f | X1) & seq is convergent & lim seq = r holds
( (f | X1) /* seq is convergent & (f | X1) /. r = lim ((f | X1) /* seq) )
then A8:
(f | X) /. r =
f /. r
by A6, PARTFUN2:15
.=
(f | X1) /. r
by A7, PARTFUN2:15
;
let s1 be
sequence of
CNS;
( rng s1 c= dom (f | X1) & s1 is convergent & lim s1 = r implies ( (f | X1) /* s1 is convergent & (f | X1) /. r = lim ((f | X1) /* s1) ) )
assume that A9:
rng s1 c= dom (f | X1)
and A10:
(
s1 is
convergent &
lim s1 = r )
;
( (f | X1) /* s1 is convergent & (f | X1) /. r = lim ((f | X1) /* s1) )
A11:
rng s1 c= dom (f | X)
by A9, A6;
(
(f | X) /* s1 is
convergent &
(f | X) /. r = lim ((f | X) /* s1) )
by A5, A10, A11;
hence
(
(f | X1) /* s1 is
convergent &
(f | X1) /. r = lim ((f | X1) /* s1) )
by A8, A12, FUNCT_2:63;
verum
end;