let CNS1, CNS2 be ComplexNormSpace; :: thesis: for X, X1 being set
for f being PartFunc of CNS1,CNS2 st f is_continuous_on X & X1 c= X holds
f is_continuous_on X1
let X, X1 be set ; :: thesis: for f being PartFunc of CNS1,CNS2 st f is_continuous_on X & X1 c= X holds
f is_continuous_on X1
let f be PartFunc of CNS1,CNS2; :: thesis: ( f is_continuous_on X & X1 c= X implies f is_continuous_on X1 )
assume A1: ( f is_continuous_on X & X1 c= X ) ; :: thesis: f is_continuous_on X1
then X c= dom f by Def21;
hence A2: X1 c= dom f by A1, XBOOLE_1:1; :: according to NCFCONT1:def 21 :: thesis: for x0 being Point of CNS1 st x0 in X1 holds
f | X1 is_continuous_in x0
let r be Point of CNS1; :: thesis: ( r in X1 implies f | X1 is_continuous_in r )
assume A3: r in X1 ; :: thesis: f | X1 is_continuous_in r
then A4: f | X is_continuous_in r by A1, Def21;
thus f | X1 is_continuous_in r :: thesis: verum

proof

r in (dom f) /\ X1 by A2, A3, XBOOLE_0:def 4;
hence A5: r in dom (f | X1) by RELAT_1:90; :: according to NCFCONT1:def 15 :: thesis: for seq being sequence of CNS1 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) )
let s1 be sequence of CNS1; :: thesis: ( 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 A6: ( rng s1 c= dom (f | X1) & s1 is convergent & lim s1 = r ) ; :: thesis: ( (f | X1) /* s1 is convergent & (f | X1) /. r = lim ((f | X1) /* s1) )
(dom f) /\ X1 c= (dom f) /\ X by A1, XBOOLE_1:26;
then dom (f | X1) c= (dom f) /\ X by RELAT_1:90;
then A7: dom (f | X1) c= dom (f | X) by RELAT_1:90;
then A8: rng s1 c= dom (f | X) by A6, XBOOLE_1:1;
then A9: ( (f | X) /* s1 is convergent & (f | X) /. r = lim ((f | X) /* s1) ) by A4, A6, Def15;
A10: (f | X) /. r = f /. r by A5, A7, PARTFUN2:32
.= (f | X1) /. r by A5, PARTFUN2:32 ;

now

let n be Element of NAT ; :: thesis: ((f | X) /* s1) . n = ((f | X1) /* s1) . n
dom s1 = NAT by FUNCT_2:def 1;
then A11: s1 . n in rng s1 by FUNCT_1:12;
thus ((f | X) /* s1) . n = (f | X) /. (s1 . n) by A6, A7, FUNCT_2:186, XBOOLE_1:1
.= f /. (s1 . n) by A8, A11, PARTFUN2:32
.= (f | X1) /. (s1 . n) by A6, A11, PARTFUN2:32
.= ((f | X1) /* s1) . n by A6, FUNCT_2:186 ; :: thesis: verum

end;

hence ( (f | X1) /* s1 is convergent & (f | X1) /. r = lim ((f | X1) /* s1) ) by A9, A10, FUNCT_2:113; :: thesis: verum

end;