let CNS be ComplexNormSpace; :: thesis:
let RNS be RealNormSpace; :: thesis:
let f be PartFunc of RNS,CNS; :: thesis:
let x0 be Point of RNS; :: thesis:
thus ( f is_continuous_in x0 implies ( x0 in dom f & ( for N1 being Neighbourhood of f /. x0 ex N being Neighbourhood of x0 st
for x1 being Point of RNS st x1 in dom f & x1 in N holds
f /. x1 in N1 ) ) ) :: thesis:

assume A1: f is_continuous_in x0 ; :: thesis:
hence x0 in dom f by Def17; :: thesis:
let N1 be Neighbourhood of f /. x0; :: thesis:
consider r being Real such that
A2: ( 0 < r & { y where y is Point of CNS : ||.(y - (f /. x0)).|| < r } c= N1 ) by Def5;
consider s being Real such that
A3: ( 0 < s & ( for x1 being Point of RNS st x1 in dom f & ||.(x1 - x0).|| < s holds
||.((f /. x1) - (f /. x0)).|| < r ) ) by A1, A2, Th31;
reconsider N = { z where z is Point of RNS : ||.(z - x0).|| < s } as Neighbourhood of x0 by A3, NFCONT_1:3;
take N ; :: thesis:
let x1 be Point of RNS; :: thesis:
assume A4: ( x1 in dom f & x1 in N ) ; :: thesis:
then consider z being Point of RNS such that
A5: x1 = z and
A6: ||.(z - x0).|| < s ;
||.((f /. x1) - (f /. x0)).|| < r by A3, A4, A5, A6;
then f /. x1 in { y where y is Point of CNS : ||.(y - (f /. x0)).|| < r } ;
hence f /. x1 in N1 by A2; :: thesis:

end;

assume A7: ( x0 in dom f & ( for N1 being Neighbourhood of f /. x0 ex N being Neighbourhood of x0 st
for x1 being Point of RNS st x1 in dom f & x1 in N holds
f /. x1 in N1 ) ) ; :: thesis:

let r be Real; :: thesis:
assume 0 < r ; :: thesis:
then reconsider N1 = { y where y is Point of CNS : ||.(y - (f /. x0)).|| < r } as Neighbourhood of f /. x0 by Th3;
consider N2 being Neighbourhood of x0 such that
A8: for x1 being Point of RNS st x1 in dom f & x1 in N2 holds
f /. x1 in N1 by A7;
consider s being Real such that
A9: ( 0 < s & { z where z is Point of RNS : ||.(z - x0).|| < s } c= N2 ) by NFCONT_1:def 3;
take s = s; :: thesis:
for x1 being Point of RNS st x1 in dom f & ||.(x1 - x0).|| < s holds
||.((f /. x1) - (f /. x0)).|| < r

let x1 be Point of RNS; :: thesis:
assume A10: ( x1 in dom f & ||.(x1 - x0).|| < s ) ; :: thesis:
then x1 in { z where z is Point of RNS : ||.(z - x0).|| < s } ;
then f /. x1 in N1 by A8, A9, A10;
then consider y being Point of CNS such that
A11: f /. x1 = y and
A12: ||.(y - (f /. x0)).|| < r ;
thus ||.((f /. x1) - (f /. x0)).|| < r by A11, A12; :: thesis:

end;

hence ( 0 < s & ( for x1 being Point of RNS st x1 in dom f & ||.(x1 - x0).|| < s holds
||.((f /. x1) - (f /. x0)).|| < r ) ) by A9; :: thesis:

end;

hence f is_continuous_in x0 by A7, Th31; :: thesis: