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;
now :: thesis: ( f is_continuous_in 0. X implies f is_continuous_on the carrier of X )
assume 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;
hence ( f is_continuous_on the carrier of X iff f is_continuous_in 0. X ) by A1, NFCONT_1:def 7; :: thesis: verum