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 x0 being Point of CNS1
for r being Real st x0 in X & 0 < r holds
ex s being Real st
( 0 < s & ( for x1 being Point of CNS1 st x1 in X & ||.(x1 - x0).|| < s holds
||.((f /. x1) - (f /. x0)).|| < r ) ) ) ) )
let X be set ; :: thesis: for f being PartFunc of CNS1,CNS2 holds
( f is_continuous_on X iff ( X c= dom f & ( for x0 being Point of CNS1
for r being Real st x0 in X & 0 < r holds
ex s being Real st
( 0 < s & ( for x1 being Point of CNS1 st x1 in X & ||.(x1 - x0).|| < s holds
||.((f /. x1) - (f /. x0)).|| < r ) ) ) ) )
let f be PartFunc of CNS1,CNS2; :: thesis: ( f is_continuous_on X iff ( X c= dom f & ( for x0 being Point of CNS1
for r being Real st x0 in X & 0 < r holds
ex s being Real st
( 0 < s & ( for x1 being Point of CNS1 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 CNS1
for r being Real st x0 in X & 0 < r holds
ex s being Real st
( 0 < s & ( for x1 being Point of CNS1 st x1 in X & ||.(x1 - x0).|| < s holds
||.((f /. x1) - (f /. x0)).|| < r ) ) ) ) ) :: thesis: ( X c= dom f & ( for x0 being Point of CNS1
for r being Real st x0 in X & 0 < r holds
ex s being Real st
( 0 < s & ( for x1 being Point of CNS1 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 CNS1
for r being Real st x0 in X & 0 < r holds
ex s being Real st
( 0 < s & ( for x1 being Point of CNS1 st x1 in X & ||.(x1 - x0).|| < s holds
||.((f /. x1) - (f /. x0)).|| < r ) ) ) )
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;
thus X c= dom f by A1, Def21; :: thesis: for x0 being Point of CNS1
for r being Real st x0 in X & 0 < r holds
ex s being Real st
( 0 < s & ( for x1 being Point of CNS1 st x1 in X & ||.(x1 - x0).|| < s holds
||.((f /. x1) - (f /. x0)).|| < r ) )
let x0 be Point of CNS1; :: thesis: for r being Real st x0 in X & 0 < r holds
ex s being Real st
( 0 < s & ( for x1 being Point of CNS1 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 CNS1 st x1 in X & ||.(x1 - x0).|| < s holds
||.((f /. x1) - (f /. x0)).|| < r ) ) )
assume A3: ( x0 in X & 0 < r ) ; :: thesis: ex s being Real st
( 0 < s & ( for x1 being Point of CNS1 st x1 in X & ||.(x1 - x0).|| < s holds
||.((f /. x1) - (f /. x0)).|| < r ) )
then f | X is_continuous_in x0 by A1, Def21;
then consider s being Real such that
A4: ( 0 < s & ( for x1 being Point of CNS1 st x1 in dom (f | X) & ||.(x1 - x0).|| < s holds
||.(((f | X) /. x1) - ((f | X) /. x0)).|| < r ) ) by A3, Th29;
A5: dom (f | X) = (dom f) /\ X by PARTFUN2:32
.= X by A2, XBOOLE_1:28 ;
take s ; :: thesis: ( 0 < s & ( for x1 being Point of CNS1 st x1 in X & ||.(x1 - x0).|| < s holds
||.((f /. x1) - (f /. x0)).|| < r ) )
thus 0 < s by A4; :: thesis: for x1 being Point of CNS1 st x1 in X & ||.(x1 - x0).|| < s holds
||.((f /. x1) - (f /. x0)).|| < r
let x1 be Point of CNS1; :: thesis: ( x1 in X & ||.(x1 - x0).|| < s implies ||.((f /. x1) - (f /. x0)).|| < r )
assume A6: ( x1 in X & ||.(x1 - x0).|| < s ) ; :: thesis: ||.((f /. x1) - (f /. x0)).|| < r
then ||.((f /. x1) - (f /. x0)).|| = ||.(((f | X) /. x1) - (f /. x0)).|| by A5, PARTFUN2:32
.= ||.(((f | X) /. x1) - ((f | X) /. x0)).|| by A3, A5, PARTFUN2:32 ;
hence ||.((f /. x1) - (f /. x0)).|| < r by A4, A5, A6; :: thesis: verum

end;

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

now

let x0 be Point of CNS1; :: thesis: ( x0 in X implies f | X is_continuous_in x0 )
assume A10: 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 CNS1 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 CNS1 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 CNS1 st x1 in dom (f | X) & ||.(x1 - x0).|| < s holds
||.(((f | X) /. x1) - ((f | X) /. x0)).|| < r ) )
then consider s being Real such that
A11: ( 0 < s & ( for x1 being Point of CNS1 st x1 in X & ||.(x1 - x0).|| < s holds
||.((f /. x1) - (f /. x0)).|| < r ) ) by A8, A10;
take s ; :: thesis: ( 0 < s & ( for x1 being Point of CNS1 st x1 in dom (f | X) & ||.(x1 - x0).|| < s holds
||.(((f | X) /. x1) - ((f | X) /. x0)).|| < r ) )
thus 0 < s by A11; :: thesis: for x1 being Point of CNS1 st x1 in dom (f | X) & ||.(x1 - x0).|| < s holds
||.(((f | X) /. x1) - ((f | X) /. x0)).|| < r
let x1 be Point of CNS1; :: thesis: ( x1 in dom (f | X) & ||.(x1 - x0).|| < s implies ||.(((f | X) /. x1) - ((f | X) /. x0)).|| < r )
assume A12: ( x1 in dom (f | X) & ||.(x1 - x0).|| < s ) ; :: thesis: ||.(((f | X) /. x1) - ((f | X) /. x0)).|| < r
||.(((f | X) /. x1) - ((f | X) /. x0)).|| = ||.(((f | X) /. x1) - (f /. x0)).|| by A9, A10, PARTFUN2:32
.= ||.((f /. x1) - (f /. x0)).|| by A12, PARTFUN2:32 ;
hence ||.(((f | X) /. x1) - ((f | X) /. x0)).|| < r by A9, A11, A12; :: thesis: verum

end;

hence f | X is_continuous_in x0 by A9, A10, Th29; :: thesis: verum

end;

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