let RNS be RealNormSpace; :: thesis: for X being set
for f being PartFunc of the carrier of RNS,COMPLEX holds
( f is_continuous_on X iff ( X c= dom f & ( for x0 being Point of RNS
for r being Real st x0 in X & 0 < r holds
ex s being Real st
( 0 < s & ( for x1 being Point of RNS st x1 in X & ||.(x1 - x0).|| < s holds
|.((f /. x1) - (f /. x0)).| < r ) ) ) ) )
let X be set ; :: thesis: for f being PartFunc of the carrier of RNS,COMPLEX holds
( f is_continuous_on X iff ( X c= dom f & ( for x0 being Point of RNS
for r being Real st x0 in X & 0 < r holds
ex s being Real st
( 0 < s & ( for x1 being Point of RNS st x1 in X & ||.(x1 - x0).|| < s holds
|.((f /. x1) - (f /. x0)).| < r ) ) ) ) )
let f be PartFunc of the carrier of RNS,COMPLEX; :: thesis: ( f is_continuous_on X iff ( X c= dom f & ( for x0 being Point of RNS
for r being Real st x0 in X & 0 < r holds
ex s being Real st
( 0 < s & ( for x1 being Point of RNS st x1 in X & ||.(x1 - x0).|| < s holds
|.((f /. x1) - (f /. x0)).| < r ) ) ) ) )
thus ( f is_continuous_on X implies ( X c= dom f & ( for x0 being Point of RNS
for r being Real st x0 in X & 0 < r holds
ex s being Real st
( 0 < s & ( for x1 being Point of RNS st x1 in X & ||.(x1 - x0).|| < s holds
|.((f /. x1) - (f /. x0)).| < r ) ) ) ) ) :: thesis: ( X c= dom f & ( for x0 being Point of RNS
for r being Real st x0 in X & 0 < r holds
ex s being Real st
( 0 < s & ( for x1 being Point of RNS st x1 in X & ||.(x1 - x0).|| < s holds
|.((f /. x1) - (f /. x0)).| < r ) ) ) implies f is_continuous_on X )

proof

assume A1: f is_continuous_on X ; :: thesis: ( X c= dom f & ( for x0 being Point of RNS
for r being Real st x0 in X & 0 < r holds
ex s being Real st
( 0 < s & ( for x1 being Point of RNS st x1 in X & ||.(x1 - x0).|| < s holds
|.((f /. x1) - (f /. x0)).| < r ) ) ) )
hence X c= dom f by Def26; :: thesis: for x0 being Point of RNS
for r being Real st x0 in X & 0 < r holds
ex s being Real st
( 0 < s & ( for x1 being Point of RNS st x1 in X & ||.(x1 - x0).|| < s holds
|.((f /. x1) - (f /. x0)).| < r ) )
A2: X c= dom f by A1, Def26;
let x0 be Point of RNS; :: thesis: for r being Real st x0 in X & 0 < r holds
ex s being Real st
( 0 < s & ( for x1 being Point of RNS st x1 in X & ||.(x1 - x0).|| < s holds
|.((f /. x1) - (f /. x0)).| < r ) )
let r be Real; :: thesis: ( x0 in X & 0 < r implies ex s being Real st
( 0 < s & ( for x1 being Point of RNS st x1 in X & ||.(x1 - x0).|| < s holds
|.((f /. x1) - (f /. x0)).| < r ) ) )
assume that
A3: x0 in X and
A4: 0 < r ; :: thesis: ex s being Real st
( 0 < s & ( for x1 being Point of RNS st x1 in X & ||.(x1 - x0).|| < s holds
|.((f /. x1) - (f /. x0)).| < r ) )
f | X is_continuous_in x0 by A1, A3, Def26;
then consider s being Real such that
A5: 0 < s and
A6: for x1 being Point of RNS st x1 in dom (f | X) & ||.(x1 - x0).|| < s holds
|.(((f | X) /. x1) - ((f | X) /. x0)).| < r by A4, Th34;
take s ; :: thesis: ( 0 < s & ( for x1 being Point of RNS st x1 in X & ||.(x1 - x0).|| < s holds
|.((f /. x1) - (f /. x0)).| < r ) )
thus 0 < s by A5; :: thesis: for x1 being Point of RNS st x1 in X & ||.(x1 - x0).|| < s holds
|.((f /. x1) - (f /. x0)).| < r
let x1 be Point of RNS; :: thesis: ( x1 in X & ||.(x1 - x0).|| < s implies |.((f /. x1) - (f /. x0)).| < r )
assume that
A7: x1 in X and
A8: ||.(x1 - x0).|| < s ; :: thesis: |.((f /. x1) - (f /. x0)).| < r
A9: dom (f | X) = (dom f) /\ X by PARTFUN2:15
.= X by A2, XBOOLE_1:28 ;
then |.((f /. x1) - (f /. x0)).| = |.(((f | X) /. x1) - (f /. x0)).| by A7, PARTFUN2:15
.= |.(((f | X) /. x1) - ((f | X) /. x0)).| by A3, A9, PARTFUN2:15 ;
hence |.((f /. x1) - (f /. x0)).| < r by A6, A9, A7, A8; :: thesis: verum

end;

assume that
A10: X c= dom f and
A11: for x0 being Point of RNS
for r being Real st x0 in X & 0 < r holds
ex s being Real st
( 0 < s & ( for x1 being Point of RNS st x1 in X & ||.(x1 - x0).|| < s holds
|.((f /. x1) - (f /. x0)).| < r ) ) ; :: thesis: f is_continuous_on X
A12: dom (f | X) = (dom f) /\ X by PARTFUN2:15
.= X by A10, XBOOLE_1:28 ;

now

let x0 be Point of RNS; :: thesis: ( x0 in X implies f | X is_continuous_in x0 )
assume A13: x0 in X ; :: thesis: f | X is_continuous_in x0
for r being Real st 0 < r holds
ex s being Real st
( 0 < s & ( for x1 being Point of RNS st x1 in dom (f | X) & ||.(x1 - x0).|| < s holds
|.(((f | X) /. x1) - ((f | X) /. x0)).| < r ) )

proof

let r be Real; :: thesis: ( 0 < r implies ex s being Real st
( 0 < s & ( for x1 being Point of RNS st x1 in dom (f | X) & ||.(x1 - x0).|| < s holds
|.(((f | X) /. x1) - ((f | X) /. x0)).| < r ) ) )
assume 0 < r ; :: thesis: ex s being Real st
( 0 < s & ( for x1 being Point of RNS st x1 in dom (f | X) & ||.(x1 - x0).|| < s holds
|.(((f | X) /. x1) - ((f | X) /. x0)).| < r ) )
then consider s being Real such that
A14: 0 < s and
A15: for x1 being Point of RNS st x1 in X & ||.(x1 - x0).|| < s holds
|.((f /. x1) - (f /. x0)).| < r by A11, A13;
take s ; :: thesis: ( 0 < s & ( for x1 being Point of RNS st x1 in dom (f | X) & ||.(x1 - x0).|| < s holds
|.(((f | X) /. x1) - ((f | X) /. x0)).| < r ) )
thus 0 < s by A14; :: thesis: for x1 being Point of RNS st x1 in dom (f | X) & ||.(x1 - x0).|| < s holds
|.(((f | X) /. x1) - ((f | X) /. x0)).| < r
let x1 be Point of RNS; :: thesis: ( x1 in dom (f | X) & ||.(x1 - x0).|| < s implies |.(((f | X) /. x1) - ((f | X) /. x0)).| < r )
assume that
A16: x1 in dom (f | X) and
A17: ||.(x1 - x0).|| < s ; :: thesis: |.(((f | X) /. x1) - ((f | X) /. x0)).| < r
|.(((f | X) /. x1) - ((f | X) /. x0)).| = |.(((f | X) /. x1) - (f /. x0)).| by A12, A13, PARTFUN2:15
.= |.((f /. x1) - (f /. x0)).| by A16, PARTFUN2:15 ;
hence |.(((f | X) /. x1) - ((f | X) /. x0)).| < r by A12, A15, A16, A17; :: thesis: verum

end;

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

end;

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