let CNS1, CNS2 be ComplexNormSpace; :: thesis: for X being set
for f being PartFunc of CNS1,CNS2 holds
( f is_continuous_on X iff ( X c= dom f & ( for s1 being sequence of CNS1 st rng s1 c= X & s1 is convergent & lim s1 in X holds
( f /* s1 is convergent & f /. (lim s1) = lim (f /* s1) ) ) ) )
let X be set ; :: thesis: for f being PartFunc of CNS1,CNS2 holds
( f is_continuous_on X iff ( X c= dom f & ( for s1 being sequence of CNS1 st rng s1 c= X & s1 is convergent & lim s1 in X holds
( f /* s1 is convergent & f /. (lim s1) = lim (f /* s1) ) ) ) )
let f be PartFunc of CNS1,CNS2; :: thesis: ( f is_continuous_on X iff ( X c= dom f & ( for s1 being sequence of CNS1 st rng s1 c= X & s1 is convergent & lim s1 in X holds
( f /* s1 is convergent & f /. (lim s1) = lim (f /* s1) ) ) ) )
thus ( f is_continuous_on X implies ( X c= dom f & ( for s1 being sequence of CNS1 st rng s1 c= X & s1 is convergent & lim s1 in X holds
( f /* s1 is convergent & f /. (lim s1) = lim (f /* s1) ) ) ) ) :: thesis: ( X c= dom f & ( for s1 being sequence of CNS1 st rng s1 c= X & s1 is convergent & lim s1 in X holds
( f /* s1 is convergent & f /. (lim s1) = lim (f /* s1) ) ) implies f is_continuous_on X )

proof

assume A1: f is_continuous_on X ; :: thesis: ( X c= dom f & ( for s1 being sequence of CNS1 st rng s1 c= X & s1 is convergent & lim s1 in X holds
( f /* s1 is convergent & f /. (lim s1) = lim (f /* s1) ) ) )
then A2: ( X c= dom f & ( for x1 being Point of CNS1 st x1 in X holds
f | X is_continuous_in x1 ) ) by Def21;

now

let s1 be sequence of CNS1; :: thesis: ( rng s1 c= X & s1 is convergent & lim s1 in X implies ( f /* s1 is convergent & f /. (lim s1) = lim (f /* s1) ) )
assume A3: ( rng s1 c= X & s1 is convergent & lim s1 in X ) ; :: thesis: ( f /* s1 is convergent & f /. (lim s1) = lim (f /* s1) )
A4: dom (f | X) = (dom f) /\ X by PARTFUN2:32
.= X by A2, XBOOLE_1:28 ;
A5: f | X is_continuous_in lim s1 by A1, A3, Def21;

now

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

end;

then A8: (f | X) /* s1 = f /* s1 by FUNCT_2:113;
f /. (lim s1) = (f | X) /. (lim s1) by A3, A4, PARTFUN2:32
.= lim (f /* s1) by A3, A4, A5, A8, Def15 ;
hence ( f /* s1 is convergent & f /. (lim s1) = lim (f /* s1) ) by A3, A4, A5, A8, Def15; :: thesis: verum

end;

hence ( X c= dom f & ( for s1 being sequence of CNS1 st rng s1 c= X & s1 is convergent & lim s1 in X holds
( f /* s1 is convergent & f /. (lim s1) = lim (f /* s1) ) ) ) by A1, Def21; :: thesis: verum

end;

assume A9: ( X c= dom f & ( for s1 being sequence of CNS1 st rng s1 c= X & s1 is convergent & lim s1 in X holds
( f /* s1 is convergent & f /. (lim s1) = lim (f /* s1) ) ) ) ; :: thesis: f is_continuous_on X

now

let x1 be Point of CNS1; :: thesis: ( x1 in X implies f | X is_continuous_in x1 )
assume A10: x1 in X ; :: thesis: f | X is_continuous_in x1
A11: dom (f | X) = (dom f) /\ X by PARTFUN2:32
.= X by A9, XBOOLE_1:28 ;

now

let s1 be sequence of CNS1; :: thesis: ( rng s1 c= dom (f | X) & s1 is convergent & lim s1 = x1 implies ( (f | X) /* s1 is convergent & (f | X) /. x1 = lim ((f | X) /* s1) ) )
assume A12: ( rng s1 c= dom (f | X) & s1 is convergent & lim s1 = x1 ) ; :: thesis: ( (f | X) /* s1 is convergent & (f | X) /. x1 = lim ((f | X) /* s1) )

now

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

end;

then A15: (f | X) /* s1 = f /* s1 by FUNCT_2:113;
(f | X) /. (lim s1) = f /. (lim s1) by A10, A11, A12, PARTFUN2:32
.= lim ((f | X) /* s1) by A9, A10, A11, A12, A15 ;
hence ( (f | X) /* s1 is convergent & (f | X) /. x1 = lim ((f | X) /* s1) ) by A9, A10, A11, A12, A15; :: thesis: verum

end;

hence f | X is_continuous_in x1 by A10, A11, Def15; :: thesis: verum

end;

hence f is_continuous_on X by A9, Def21; :: thesis: verum