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;

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 A8:
f is_continuous_in 0. X
; :: thesis: f is_continuous_in xassume A3:
f is_continuous_in x
; :: thesis: f is_continuous_in 0. X

end;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 ) )

hence
f is_continuous_in 0. X
by A1, NFCONT_1:7; :: thesis: verumex 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 A3, NFCONT_1:7;

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 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: verum

end;( 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 A3, NFCONT_1:7;

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 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: verum

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 ) )

hence
f is_continuous_in x
by A1, NFCONT_1:7; :: thesis: verumex 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 A8, NFCONT_1:7;

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

end;( 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 A8, NFCONT_1:7;

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 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: verum

end;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 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: verum