let X, X1 be set ; :: thesis: for S being RealNormSpace
for f being PartFunc of REAL, the carrier of S st f | X is Lipschitzian & X1 c= X holds
f | X1 is Lipschitzian
let S be RealNormSpace; :: thesis: for f being PartFunc of REAL, the carrier of S st f | X is Lipschitzian & X1 c= X holds
f | X1 is Lipschitzian
let f be PartFunc of REAL, the carrier of S; :: 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