let X, X1 be set ; :: thesis: for f being PartFunc of REAL ,REAL st f | X is Lipschitzian & X1 c= X holds
f | X1 is Lipschitzian
let f be PartFunc of REAL ,REAL ; :: thesis: ( f | X is Lipschitzian & X1 c= X implies f | X1 is Lipschitzian )
assume A1: ( f | X is Lipschitzian & X1 c= X ) ; :: thesis: f | X1 is Lipschitzian
then f | X1 = (f | X) | X1 by RELAT_1:103;
hence f | X1 is Lipschitzian by A1; :: thesis: verum