let X, Y be RealNormSpace; :: thesis: for f being Function of (TopSpaceNorm X),(TopSpaceNorm Y)
for ft being Function of (LinearTopSpaceNorm X),(LinearTopSpaceNorm Y) st f = ft holds
( f is continuous iff ft is continuous )
let f be Function of (TopSpaceNorm X),(TopSpaceNorm Y); :: thesis: for ft being Function of (LinearTopSpaceNorm X),(LinearTopSpaceNorm Y) st f = ft holds
( f is continuous iff ft is continuous )
let ft be Function of (LinearTopSpaceNorm X),(LinearTopSpaceNorm Y); :: thesis: ( f = ft implies ( f is continuous iff ft is continuous ) )
assume A1: f = ft ; :: thesis: ( f is continuous iff ft is continuous )

hereby :: thesis: ( ft is continuous implies f is continuous )

assume A2: f is continuous ; :: thesis: ft is continuous

now :: thesis: for xt being Point of (LinearTopSpaceNorm X) holds ft is_continuous_at xt

let xt be Point of (LinearTopSpaceNorm X); :: thesis: ft is_continuous_at xt
reconsider x = xt as Point of (TopSpaceNorm X) by Def4;
f is_continuous_at x by A2, TMAP_1:44;
hence ft is_continuous_at xt by A1, Th35; :: thesis: verum

end;

hence ft is continuous by TMAP_1:44; :: thesis: verum

end;

assume A3: ft is continuous ; :: thesis: f is continuous

now :: thesis: for x being Point of (TopSpaceNorm X) holds f is_continuous_at x

let x be Point of (TopSpaceNorm X); :: thesis: f is_continuous_at x
reconsider xt = x as Point of (LinearTopSpaceNorm X) by Def4;
ft is_continuous_at xt by A3, TMAP_1:44;
hence f is_continuous_at x by A1, Th35; :: thesis: verum

end;

hence f is continuous by TMAP_1:44; :: thesis: verum