let X, X1 be set ; :: thesis: for f being PartFunc of REAL,REAL st f | X is continuous & X1 c= X holds

f | X1 is continuous

let f be PartFunc of REAL,REAL; :: thesis: ( f | X is continuous & X1 c= X implies f | X1 is continuous )

assume A1: f | X is continuous ; :: thesis: ( not X1 c= X or f | X1 is continuous )

assume X1 c= X ; :: thesis: f | X1 is continuous

then f | X1 = (f | X) | X1 by RELAT_1:74;

hence f | X1 is continuous by A1; :: thesis: verum

f | X1 is continuous

let f be PartFunc of REAL,REAL; :: thesis: ( f | X is continuous & X1 c= X implies f | X1 is continuous )

assume A1: f | X is continuous ; :: thesis: ( not X1 c= X or f | X1 is continuous )

assume X1 c= X ; :: thesis: f | X1 is continuous

then f | X1 = (f | X) | X1 by RELAT_1:74;

hence f | X1 is continuous by A1; :: thesis: verum