let CNS be ComplexNormSpace; :: thesis: for RNS being RealNormSpace
for f being PartFunc of RNS,CNS
for x0 being Point of RNS st x0 in dom f holds
f is_continuous_on {x0}
let RNS be RealNormSpace; :: thesis: for f being PartFunc of RNS,CNS
for x0 being Point of RNS st x0 in dom f holds
f is_continuous_on {x0}
let f be PartFunc of RNS,CNS; :: thesis: for x0 being Point of RNS st x0 in dom f holds
f is_continuous_on {x0}
let x0 be Point of RNS; :: thesis: ( x0 in dom f implies f is_continuous_on {x0} )
assume A1: x0 in dom f ; :: thesis: f is_continuous_on {x0}
thus {x0} c= dom f by A1, TARSKI:def 1; :: according to NCFCONT1:def 13 :: thesis: for x0 being Point of RNS st x0 in {x0} holds
f | {x0} is_continuous_in x0
let p be Point of RNS; :: thesis: ( p in {x0} implies f | {x0} is_continuous_in p )
assume A2: p in {x0} ; :: thesis: f | {x0} is_continuous_in p
thus f | {x0} is_continuous_in p :: thesis: verum

proof

p in dom f by A1, A2, TARSKI:def 1;
then p in (dom f) /\ {x0} by A2, XBOOLE_0:def 4;
hence p in dom (f | {x0}) by RELAT_1:61; :: according to NCFCONT1:def 7 :: thesis: for seq being sequence of RNS st rng seq c= dom (f | {x0}) & seq is convergent & lim seq = p holds
( (f | {x0}) /* seq is convergent & (f | {x0}) /. p = lim ((f | {x0}) /* seq) )
let s1 be sequence of RNS; :: thesis: ( rng s1 c= dom (f | {x0}) & s1 is convergent & lim s1 = p implies ( (f | {x0}) /* s1 is convergent & (f | {x0}) /. p = lim ((f | {x0}) /* s1) ) )
assume that
A3: rng s1 c= dom (f | {x0}) and
s1 is convergent and
lim s1 = p ; :: thesis: ( (f | {x0}) /* s1 is convergent & (f | {x0}) /. p = lim ((f | {x0}) /* s1) )
A4: (dom f) /\ {x0} c= {x0} by XBOOLE_1:17;
rng s1 c= (dom f) /\ {x0} by A3, RELAT_1:61;
then A5: rng s1 c= {x0} by A4;

A6: now :: thesis: for n being Element of NAT holds s1 . n = x0

let n be Element of NAT ; :: thesis: s1 . n = x0
dom s1 = NAT by FUNCT_2:def 1;
then s1 . n in rng s1 by FUNCT_1:3;
hence s1 . n = x0 by A5, TARSKI:def 1; :: thesis: verum

end;

A7: p = x0 by A2, TARSKI:def 1;

A8: now :: thesis: for g being Real st 0 < g holds
ex n being Nat st
for m being Nat st n <= m holds
||.((((f | {x0}) /* s1) . m) - ((f | {x0}) /. p)).|| < g

let g be Real; :: thesis: ( 0 < g implies ex n being Nat st
for m being Nat st n <= m holds
||.((((f | {x0}) /* s1) . m) - ((f | {x0}) /. p)).|| < g )
assume A9: 0 < g ; :: thesis: ex n being Nat st
for m being Nat st n <= m holds
||.((((f | {x0}) /* s1) . m) - ((f | {x0}) /. p)).|| < g
reconsider n = 0 as Nat ;
take n = n; :: thesis: for m being Nat st n <= m holds
||.((((f | {x0}) /* s1) . m) - ((f | {x0}) /. p)).|| < g
let m be Nat; :: thesis: ( n <= m implies ||.((((f | {x0}) /* s1) . m) - ((f | {x0}) /. p)).|| < g )
assume n <= m ; :: thesis: ||.((((f | {x0}) /* s1) . m) - ((f | {x0}) /. p)).|| < g
A10: m in NAT by ORDINAL1:def 12;
||.((((f | {x0}) /* s1) . m) - ((f | {x0}) /. p)).|| = ||.(((f | {x0}) /. (s1 . m)) - ((f | {x0}) /. x0)).|| by A7, A3, FUNCT_2:109, A10
.= ||.(((f | {x0}) /. x0) - ((f | {x0}) /. x0)).|| by A6, A10
.= ||.(0. CNS).|| by RLVECT_1:15
.= 0 by CLVECT_1:102 ;
hence ||.((((f | {x0}) /* s1) . m) - ((f | {x0}) /. p)).|| < g by A9; :: thesis: verum

end;

hence (f | {x0}) /* s1 is convergent by CLVECT_1:def 15; :: thesis: (f | {x0}) /. p = lim ((f | {x0}) /* s1)
hence (f | {x0}) /. p = lim ((f | {x0}) /* s1) by A8, CLVECT_1:def 16; :: thesis: verum

end;