let X, Y, Z be non empty TopSpace; :: thesis: ( the carrier of X = the carrier of Y & the topology of Y c= the topology of X implies for f being continuous Function of Y,Z holds f is continuous Function of X,Z )

assume that

A1: the carrier of X = the carrier of Y and

A2: the topology of Y c= the topology of X ; :: thesis: for f being continuous Function of Y,Z holds f is continuous Function of X,Z

let f be continuous Function of Y,Z; :: 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 by A1, Th44, A2, Th46;

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

assume that

A1: the carrier of X = the carrier of Y and

A2: the topology of Y c= the topology of X ; :: thesis: for f being continuous Function of Y,Z holds f is continuous Function of X,Z

let f be continuous Function of Y,Z; :: 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 by A1, Th44, A2, Th46;

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