let X, Y be RealNormSpace; :: thesis:
let f be LinearOperator of X,Y; :: thesis:
let x be Point of X; :: thesis:
A1: dom f = the carrier of X by FUNCT_2:def 1;
A2: 0. Y = f /. (0. X) by Th3;

hereby :: thesis:

assume A3: f is_continuous_in x ; :: thesis:

now :: thesis:

let r be Real; :: thesis:
assume 0 < r ; :: thesis:
then consider s being Real such that
A4: ( 0 < s & ( for x1 being Point of X st x1 in dom f & ||.(x1 - x).|| < s holds
||.((f /. x1) - (f /. x)).|| < r ) ) by A3, NFCONT_1:7;
take s = s; :: thesis:
thus 0 < s by A4; :: thesis:
let x1 be Point of X; :: thesis:
assume A5: ( x1 in dom f & ||.(x1 - (0. X)).|| < s ) ; :: thesis:
set y1 = x1 + x;
A6: (x1 + x) - x = x1 + (x - x) by RLVECT_1:28
.= x1 + (0. X) by RLVECT_1:15
.= x1 by RLVECT_1:4 ;
then A7: ||.((x1 + x) - x).|| < s by A5, RLVECT_1:13;
(f /. (x1 + x)) - (f /. x) = (f . (x1 + x)) + ((- 1) * (f . x)) by RLVECT_1:16
.= (f . (x1 + x)) + (f . ((- 1) * x)) by LOPBAN_1:def 5
.= f . ((x1 + x) + ((- 1) * x)) by VECTSP_1:def 20
.= f . ((x1 + x) - x) by RLVECT_1:16
.= (f /. x1) - (f /. (0. X)) by A6, A2, RLVECT_1:13 ;
hence ||.((f /. x1) - (f /. (0. X))).|| < r by A7, A4, A1; :: thesis:

end;

hence f is_continuous_in 0. X by A1, NFCONT_1:7; :: thesis:

end;

assume A8: f is_continuous_in 0. X ; :: thesis:

now :: thesis:

let r be Real; :: thesis:
assume 0 < r ; :: thesis:
then consider s being Real such that
A9: ( 0 < s & ( for x1 being Point of X st x1 in dom f & ||.(x1 - (0. X)).|| < s holds
||.((f /. x1) - (f /. (0. X))).|| < r ) ) by A8, NFCONT_1:7;
take s = s; :: thesis:
thus 0 < s by A9; :: thesis:
thus for x1 being Point of X st x1 in dom f & ||.(x1 - x).|| < s holds
||.((f /. x1) - (f /. x)).|| < r :: thesis:

proof

let x1 be Point of X; :: thesis:
assume A10: ( x1 in dom f & ||.(x1 - x).|| < s ) ; :: thesis:
set y1 = x1 - x;
A11: ||.((x1 - x) - (0. X)).|| < s by A10, RLVECT_1:13;
(f /. (x1 - x)) - (f /. (0. X)) = f . (x1 - x) by A2, RLVECT_1:13
.= f . (x1 + ((- 1) * x)) by RLVECT_1:16
.= (f . x1) + (f . ((- 1) * x)) by VECTSP_1:def 20
.= (f . x1) + ((- 1) * (f . x)) by LOPBAN_1:def 5
.= (f . x1) - (f . x) by RLVECT_1:16 ;
hence ||.((f /. x1) - (f /. x)).|| < r by A11, A9, A1; :: thesis:

end;

end;

hence f is_continuous_in x by A1, NFCONT_1:7; :: thesis: