let T be TopStruct ; :: thesis: for f being RealMap of T
for g being Function of T,R^1 st f = g holds
( f is continuous iff g is continuous )
let f be RealMap of T; :: thesis: for g being Function of T,R^1 st f = g holds
( f is continuous iff g is continuous )
let g be Function of T,R^1; :: thesis: ( f = g implies ( f is continuous iff g is continuous ) )
assume A1: f = g ; :: thesis: ( f is continuous iff g is continuous )
thus ( f is continuous implies g is continuous ) :: thesis: ( g is continuous implies f is continuous )
proof
assume A2: for Y being Subset of REAL st Y is closed holds
f " Y is closed ; :: according to PSCOMP_1:def 3 :: thesis: g is continuous
let P be Subset of R^1; :: according to PRE_TOPC:def 6 :: thesis: ( not P is closed or g " P is closed )
assume A3: P is closed ; :: thesis: g " P is closed
reconsider R = P as Subset of REAL by TOPMETR:17;
R is closed by A3, Th23;
hence g " P is closed by A1, A2; :: thesis: verum
end;
assume A4: for Y being Subset of R^1 st Y is closed holds
g " Y is closed ; :: according to PRE_TOPC:def 6 :: thesis: f is continuous
let P be Subset of REAL; :: according to PSCOMP_1:def 3 :: thesis: ( not P is closed or f " P is closed )
assume A5: P is closed ; :: thesis: f " P is closed
reconsider R = P as Subset of R^1 by TOPMETR:17;
R is closed by A5, Th23;
hence f " P is closed by A1, A4; :: thesis: verum