let X be set ; :: thesis: for f being PartFunc of REAL,REAL holds
( f | X is Lipschitzian iff ex r being real number st
( 0 < r & ( for x1, x2 being real number st x1 in dom (f | X) & x2 in dom (f | X) holds
abs ((f . x1) - (f . x2)) <= r * (abs (x1 - x2)) ) ) )
let f be PartFunc of REAL,REAL; :: thesis: ( f | X is Lipschitzian iff ex r being real number st
( 0 < r & ( for x1, x2 being real number st x1 in dom (f | X) & x2 in dom (f | X) holds
abs ((f . x1) - (f . x2)) <= r * (abs (x1 - x2)) ) ) )
thus ( f | X is Lipschitzian implies ex r being real number st
( 0 < r & ( for x1, x2 being real number st x1 in dom (f | X) & x2 in dom (f | X) holds
abs ((f . x1) - (f . x2)) <= r * (abs (x1 - x2)) ) ) ) :: thesis: ( ex r being real number st
( 0 < r & ( for x1, x2 being real number st x1 in dom (f | X) & x2 in dom (f | X) holds
abs ((f . x1) - (f . x2)) <= r * (abs (x1 - x2)) ) ) implies f | X is Lipschitzian )

proof

given r being real number such that A1: 0 < r and
A2: for x1, x2 being real number st x1 in dom (f | X) & x2 in dom (f | X) holds
abs (((f | X) . x1) - ((f | X) . x2)) <= r * (abs (x1 - x2)) ; :: according to FCONT_1:def 3 :: thesis: ex r being real number st
( 0 < r & ( for x1, x2 being real number st x1 in dom (f | X) & x2 in dom (f | X) holds
abs ((f . x1) - (f . x2)) <= r * (abs (x1 - x2)) ) )
take r ; :: thesis: ( 0 < r & ( for x1, x2 being real number st x1 in dom (f | X) & x2 in dom (f | X) holds
abs ((f . x1) - (f . x2)) <= r * (abs (x1 - x2)) ) )
thus 0 < r by A1; :: thesis: for x1, x2 being real number st x1 in dom (f | X) & x2 in dom (f | X) holds
abs ((f . x1) - (f . x2)) <= r * (abs (x1 - x2))
let x1, x2 be real number ; :: thesis: ( x1 in dom (f | X) & x2 in dom (f | X) implies abs ((f . x1) - (f . x2)) <= r * (abs (x1 - x2)) )
assume A3: ( x1 in dom (f | X) & x2 in dom (f | X) ) ; :: thesis: abs ((f . x1) - (f . x2)) <= r * (abs (x1 - x2))
then ( (f | X) . x1 = f . x1 & (f | X) . x2 = f . x2 ) by FUNCT_1:47;
hence abs ((f . x1) - (f . x2)) <= r * (abs (x1 - x2)) by A2, A3; :: thesis: verum

end;

given r being real number such that A4: 0 < r and
A5: for x1, x2 being real number st x1 in dom (f | X) & x2 in dom (f | X) holds
abs ((f . x1) - (f . x2)) <= r * (abs (x1 - x2)) ; :: thesis: f | X is Lipschitzian
take r ; :: according to FCONT_1:def 3 :: thesis: ( 0 < r & ( for x1, x2 being real number st x1 in dom (f | X) & x2 in dom (f | X) holds
abs (((f | X) . x1) - ((f | X) . x2)) <= r * (abs (x1 - x2)) ) )
thus 0 < r by A4; :: thesis: for x1, x2 being real number st x1 in dom (f | X) & x2 in dom (f | X) holds
abs (((f | X) . x1) - ((f | X) . x2)) <= r * (abs (x1 - x2))
let x1, x2 be real number ; :: thesis: ( x1 in dom (f | X) & x2 in dom (f | X) implies abs (((f | X) . x1) - ((f | X) . x2)) <= r * (abs (x1 - x2)) )
assume A6: ( x1 in dom (f | X) & x2 in dom (f | X) ) ; :: thesis: abs (((f | X) . x1) - ((f | X) . x2)) <= r * (abs (x1 - x2))
then ( (f | X) . x1 = f . x1 & (f | X) . x2 = f . x2 ) by FUNCT_1:47;
hence abs (((f | X) . x1) - ((f | X) . x2)) <= r * (abs (x1 - x2)) by A5, A6; :: thesis: verum