now

let Y be Subset of REAL ; :: thesis: ( Y is open implies (f | X) " Y is open )
assume Y is open ; :: thesis: (f | X) " Y is open
then A1: f " Y is open by Th54;
A2: the carrier of (T | X) = X by PRE_TOPC:29;
(f | X) " Y = X /\ (f " Y) by FUNCT_1:139;
hence (f | X) " Y is open by A1, A2, TSP_1:def 1; :: thesis: verum

end;

hence f | X is continuous RealMap of (T | X) by Th54; :: thesis: verum