let X, Y be RealNormSpace; :: thesis: for f being LinearOperator of X,Y
for x being Point of X holds
( f is_continuous_in x iff f is_continuous_in 0. X )

let f be LinearOperator of X,Y; :: thesis: for x being Point of X holds
( f is_continuous_in x iff f is_continuous_in 0. X )

let x be Point of X; :: thesis: ( f is_continuous_in x iff f is_continuous_in 0. X )
A1: dom f = the carrier of X by FUNCT_2:def 1;
A2: 0. Y = f /. (0. X) by Th3;
hereby :: thesis: ( f is_continuous_in 0. X implies f is_continuous_in x )
assume A3: f is_continuous_in x ; :: thesis:
now :: thesis: for r being Real st 0 < r holds
ex s being Real st
( 0 < s & ( for x1 being Point of X st x1 in dom f & ||.(x1 - (0. X)).|| < s holds
||.((f /. x1) - (f /. (0. X))).|| < r ) )
let r be Real; :: thesis: ( 0 < r implies ex s being Real st
( 0 < s & ( for x1 being Point of X st x1 in dom f & ||.(x1 - (0. X)).|| < s holds
||.((f /. x1) - (f /. (0. X))).|| < r ) ) )

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

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 ;
take s = s; :: thesis: ( 0 < s & ( for x1 being Point of X st x1 in dom f & ||.(x1 - (0. X)).|| < s holds
||.((f /. x1) - (f /. (0. X))).|| < r ) )

thus 0 < s by A4; :: thesis: for x1 being Point of X st x1 in dom f & ||.(x1 - (0. X)).|| < s holds
||.((f /. x1) - (f /. (0. X))).|| < r

let x1 be Point of X; :: thesis: ( x1 in dom f & ||.(x1 - (0. X)).|| < s implies ||.((f /. x1) - (f /. (0. X))).|| < r )
assume A5: ( x1 in dom f & ||.(x1 - (0. X)).|| < s ) ; :: thesis: ||.((f /. x1) - (f /. (0. X))).|| < r
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 ;
(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 ;
hence ||.((f /. x1) - (f /. (0. X))).|| < r by A7, A4, A1; :: thesis: verum
end;
hence f is_continuous_in 0. X by ; :: thesis: verum
end;
assume A8: f is_continuous_in 0. X ; :: thesis:
now :: thesis: for r being Real st 0 < r holds
ex s being Real st
( 0 < s & ( for x1 being Point of X st x1 in dom f & ||.(x1 - x).|| < s holds
||.((f /. x1) - (f /. x)).|| < r ) )
let r be Real; :: thesis: ( 0 < r implies ex s being Real st
( 0 < s & ( for x1 being Point of X st x1 in dom f & ||.(x1 - x).|| < s holds
||.((f /. x1) - (f /. x)).|| < r ) ) )

assume 0 < r ; :: thesis: ex s being Real st
( 0 < s & ( for x1 being Point of X st x1 in dom f & ||.(x1 - x).|| < s holds
||.((f /. x1) - (f /. x)).|| < r ) )

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 ;
take s = s; :: thesis: ( 0 < s & ( for x1 being Point of X st x1 in dom f & ||.(x1 - x).|| < s holds
||.((f /. x1) - (f /. x)).|| < r ) )

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

thus for x1 being Point of X st x1 in dom f & ||.(x1 - x).|| < s holds
||.((f /. x1) - (f /. x)).|| < r :: thesis: verum
proof
let x1 be Point of X; :: thesis: ( x1 in dom f & ||.(x1 - x).|| < s implies ||.((f /. x1) - (f /. x)).|| < r )
assume A10: ( x1 in dom f & ||.(x1 - x).|| < s ) ; :: thesis: ||.((f /. x1) - (f /. x)).|| < r
set y1 = x1 - x;
A11: ||.((x1 - x) - (0. X)).|| < s by ;
(f /. (x1 - x)) - (f /. (0. X)) = f . (x1 - x) by
.= 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: verum
end;
end;
hence f is_continuous_in x by ; :: thesis: verum