let X, Y, Z be non empty TopSpace; :: thesis: ( the carrier of Y = the carrier of Z & the topology of Z c= the topology of Y implies for f being continuous Function of X,Y holds f is continuous Function of X,Z )
assume that
A1: the carrier of Y = the carrier of Z and
A2: the topology of Z c= the topology of Y ; :: thesis: for f being continuous Function of X,Y holds f is continuous Function of X,Z
let f be continuous Function of X,Y; :: thesis: f is continuous Function of X,Z
reconsider g = f as Function of X,Z by A1;
for x being Point of X holds g is_continuous_at x

proof

let x be Point of X; :: thesis: g is_continuous_at x
f is_continuous_at x by Th49;
hence g is_continuous_at x by A1, A2, Th50; :: thesis: verum

end;

hence f is continuous Function of X,Z by Th49; :: thesis: verum