let n be Element of NAT ; :: thesis: for X, X1 being set

for f being PartFunc of REAL,(REAL n) st f | X is Lipschitzian & X1 c= X holds

f | X1 is Lipschitzian

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

f | X1 is Lipschitzian

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

assume that

A1: f | X is Lipschitzian and

A2: X1 c= X ; :: thesis: f | X1 is Lipschitzian

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

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

for f being PartFunc of REAL,(REAL n) st f | X is Lipschitzian & X1 c= X holds

f | X1 is Lipschitzian

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

f | X1 is Lipschitzian

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

assume that

A1: f | X is Lipschitzian and

A2: X1 c= X ; :: thesis: f | X1 is Lipschitzian

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

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