let CNS be ComplexNormSpace; :: thesis: for RNS being RealNormSpace
for X being set
for f being PartFunc of RNS,CNS holds
( f is_continuous_on X iff ( X c= dom f & ( for s1 being sequence of RNS st rng s1 c= X & s1 is convergent & lim s1 in X holds
( f /* s1 is convergent & f /. (lim s1) = lim (f /* s1) ) ) ) )
let RNS be RealNormSpace; :: thesis: for X being set
for f being PartFunc of RNS,CNS holds
( f is_continuous_on X iff ( X c= dom f & ( for s1 being sequence of RNS 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 RNS,CNS holds
( f is_continuous_on X iff ( X c= dom f & ( for s1 being sequence of RNS 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 RNS,CNS; :: thesis: ( f is_continuous_on X iff ( X c= dom f & ( for s1 being sequence of RNS 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 RNS 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 RNS 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 RNS 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 ;

now :: thesis: for s1 being sequence of RNS st rng s1 c= X & s1 is convergent & lim s1 in X holds
( f /* s1 is convergent & f /. (lim s1) = lim (f /* s1) )

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

now :: thesis: for n being Element of NAT holds ((f | X) /* s1) . n = (f /* s1) . n

let n be Element of NAT ; :: thesis: ((f | X) /* s1) . n = (f /* s1) . n
dom s1 = NAT by FUNCT_2:def 1;
then A8: s1 . n in rng s1 by FUNCT_1:3;
thus ((f | X) /* s1) . n = (f | X) /. (s1 . n) by A3, A7, FUNCT_2:109
.= f /. (s1 . n) by A3, A7, A8, PARTFUN2:15
.= (f /* s1) . n by A2, A3, FUNCT_2:109, XBOOLE_1:1 ; :: thesis: verum

end;

then A9: (f | X) /* s1 = f /* s1 by FUNCT_2:63;
f /. (lim s1) = (f | X) /. (lim s1) by A5, A7, PARTFUN2:15
.= lim (f /* s1) by A3, A4, A7, A6, A9 ;
hence ( f /* s1 is convergent & f /. (lim s1) = lim (f /* s1) ) by A3, A4, A7, A6, A9; :: thesis: verum

end;

hence ( X c= dom f & ( for s1 being sequence of RNS 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; :: thesis: verum

end;

assume that
A10: X c= dom f and
A11: for s1 being sequence of RNS 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 :: thesis: for x1 being Point of RNS st x1 in X holds
f | X is_continuous_in x1

A12: dom (f | X) = (dom f) /\ X by PARTFUN2:15
.= X by A10, XBOOLE_1:28 ;
let x1 be Point of RNS; :: thesis: ( x1 in X implies f | X is_continuous_in x1 )
assume A13: x1 in X ; :: thesis: f | X is_continuous_in x1

now :: thesis: for s1 being sequence of RNS st rng s1 c= dom (f | X) & s1 is convergent & lim s1 = x1 holds
( (f | X) /* s1 is convergent & (f | X) /. x1 = lim ((f | X) /* s1) )

let s1 be sequence of RNS; :: 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 that
A14: rng s1 c= dom (f | X) and
A15: s1 is convergent and
A16: lim s1 = x1 ; :: thesis: ( (f | X) /* s1 is convergent & (f | X) /. x1 = lim ((f | X) /* s1) )

now :: thesis: for n being Element of NAT holds ((f | X) /* s1) . n = (f /* s1) . n

let n be Element of NAT ; :: thesis: ((f | X) /* s1) . n = (f /* s1) . n
dom s1 = NAT by FUNCT_2:def 1;
then A17: s1 . n in rng s1 by FUNCT_1:3;
thus ((f | X) /* s1) . n = (f | X) /. (s1 . n) by A14, FUNCT_2:109
.= f /. (s1 . n) by A14, A17, PARTFUN2:15
.= (f /* s1) . n by A10, A12, A14, FUNCT_2:109, XBOOLE_1:1 ; :: thesis: verum

end;

then A18: (f | X) /* s1 = f /* s1 by FUNCT_2:63;
(f | X) /. (lim s1) = f /. (lim s1) by A13, A12, A16, PARTFUN2:15
.= lim ((f | X) /* s1) by A11, A13, A12, A14, A15, A16, A18 ;
hence ( (f | X) /* s1 is convergent & (f | X) /. x1 = lim ((f | X) /* s1) ) by A11, A13, A12, A14, A15, A16, A18; :: thesis: verum

end;

hence f | X is_continuous_in x1 by A13, A12; :: thesis: verum

end;

hence f is_continuous_on X by A10; :: thesis: verum