let X be RealUnitarySpace; :: thesis: for f being Function of X,REAL
for g being Function of (),REAL st f = g holds
( f is_Lipschitzian_on the carrier of X iff g is_Lipschitzian_on the carrier of () )

let f be Function of X,REAL; :: thesis: for g being Function of (),REAL st f = g holds
( f is_Lipschitzian_on the carrier of X iff g is_Lipschitzian_on the carrier of () )

let g be Function of (),REAL; :: thesis: ( f = g implies ( f is_Lipschitzian_on the carrier of X iff g is_Lipschitzian_on the carrier of () ) )
assume AS: f = g ; :: thesis: ( f is_Lipschitzian_on the carrier of X iff g is_Lipschitzian_on the carrier of () )
set Y = RUSp2RNSp X;
thus ( f is_Lipschitzian_on the carrier of X implies g is_Lipschitzian_on the carrier of () ) :: thesis: ( g is_Lipschitzian_on the carrier of () implies f is_Lipschitzian_on the carrier of X )
proof
assume A11: f is_Lipschitzian_on the carrier of X ; :: thesis: g is_Lipschitzian_on the carrier of ()
then consider r being Real such that
A2: ( 0 < r & ( for x1, x2 being Point of X st x1 in the carrier of X & x2 in the carrier of X holds
|.((f /. x1) - (f /. x2)).| <= r * ||.(x1 - x2).|| ) ) ;
for y1, y2 being Point of () st y1 in the carrier of () & y2 in the carrier of () holds
|.((g /. y1) - (g /. y2)).| <= r * ||.(y1 - y2).||
proof
let y1, y2 be Point of (); :: thesis: ( y1 in the carrier of () & y2 in the carrier of () implies |.((g /. y1) - (g /. y2)).| <= r * ||.(y1 - y2).|| )
assume ( y1 in the carrier of () & y2 in the carrier of () ) ; :: thesis: |.((g /. y1) - (g /. y2)).| <= r * ||.(y1 - y2).||
reconsider x1 = y1, x2 = y2 as Point of X ;
||.(y1 - y2).|| = ||.(x1 - x2).|| by ;
hence |.((g /. y1) - (g /. y2)).| <= r * ||.(y1 - y2).|| by A2, AS; :: thesis: verum
end;
hence g is_Lipschitzian_on the carrier of () by A2, A11, AS; :: thesis: verum
end;
assume A11: g is_Lipschitzian_on the carrier of () ; :: thesis: f is_Lipschitzian_on the carrier of X
then consider r being Real such that
A2: ( 0 < r & ( for y1, y2 being Point of () st y1 in the carrier of () & y2 in the carrier of () holds
|.((g /. y1) - (g /. y2)).| <= r * ||.(y1 - y2).|| ) ) ;
for x1, x2 being Point of X st x1 in the carrier of X & x2 in the carrier of X holds
|.((f /. x1) - (f /. x2)).| <= r * ||.(x1 - x2).||
proof
let x1, x2 be Point of X; :: thesis: ( x1 in the carrier of X & x2 in the carrier of X implies |.((f /. x1) - (f /. x2)).| <= r * ||.(x1 - x2).|| )
assume ( x1 in the carrier of X & x2 in the carrier of X ) ; :: thesis: |.((f /. x1) - (f /. x2)).| <= r * ||.(x1 - x2).||
reconsider y1 = x1, y2 = x2 as Point of () ;
||.(x1 - x2).|| = ||.(y1 - y2).|| by ;
hence |.((f /. x1) - (f /. x2)).| <= r * ||.(x1 - x2).|| by A2, AS; :: thesis: verum
end;
hence f is_Lipschitzian_on the carrier of X by A2, A11, AS; :: thesis: verum