let X, Y be RealNormSpace; :: thesis: for f being LinearOperator of X,Y holds

( f is_continuous_on the carrier of X iff f is_continuous_in 0. X )

let f be LinearOperator of X,Y; :: thesis: ( f is_continuous_on the carrier of X iff f is_continuous_in 0. X )

A1: f | the carrier of X = f ;

A2: dom f = the carrier of X by FUNCT_2:def 1;

( f is_continuous_on the carrier of X iff f is_continuous_in 0. X )

let f be LinearOperator of X,Y; :: thesis: ( f is_continuous_on the carrier of X iff f is_continuous_in 0. X )

A1: f | the carrier of X = f ;

A2: dom f = the carrier of X by FUNCT_2:def 1;

now :: thesis: ( f is_continuous_in 0. X implies f is_continuous_on the carrier of X )

hence
( f is_continuous_on the carrier of X iff f is_continuous_in 0. X )
by A1, NFCONT_1:def 7; :: thesis: verumassume A3:
f is_continuous_in 0. X
; :: thesis: f is_continuous_on the carrier of X

for x being Point of X st x in the carrier of X holds

f | the carrier of X is_continuous_in x by A3, Th4;

hence f is_continuous_on the carrier of X by A2, NFCONT_1:def 7; :: thesis: verum

end;for x being Point of X st x in the carrier of X holds

f | the carrier of X is_continuous_in x by A3, Th4;

hence f is_continuous_on the carrier of X by A2, NFCONT_1:def 7; :: thesis: verum