let X be RealUnitarySpace; :: thesis: for f being Function of X,REAL
for g being Function of (RUSp2RNSp X),REAL st f = g holds
( f is_Lipschitzian_on the carrier of X iff g is_Lipschitzian_on the carrier of (RUSp2RNSp X) )
let f be Function of X,REAL; :: thesis: for g being Function of (RUSp2RNSp X),REAL st f = g holds
( f is_Lipschitzian_on the carrier of X iff g is_Lipschitzian_on the carrier of (RUSp2RNSp X) )
let g be Function of (RUSp2RNSp X),REAL; :: thesis: ( f = g implies ( f is_Lipschitzian_on the carrier of X iff g is_Lipschitzian_on the carrier of (RUSp2RNSp X) ) )
assume AS: f = g ; :: thesis: ( f is_Lipschitzian_on the carrier of X iff g is_Lipschitzian_on the carrier of (RUSp2RNSp X) )
set Y = RUSp2RNSp X;
thus ( f is_Lipschitzian_on the carrier of X implies g is_Lipschitzian_on the carrier of (RUSp2RNSp X) ) :: thesis: ( g is_Lipschitzian_on the carrier of (RUSp2RNSp X) 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 (RUSp2RNSp X)
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 (RUSp2RNSp X) st y1 in the carrier of (RUSp2RNSp X) & y2 in the carrier of (RUSp2RNSp X) holds
|.((g /. y1) - (g /. y2)).| <= r * ||.(y1 - y2).||

proof

let y1, y2 be Point of (RUSp2RNSp X); :: thesis: ( y1 in the carrier of (RUSp2RNSp X) & y2 in the carrier of (RUSp2RNSp X) implies |.((g /. y1) - (g /. y2)).| <= r * ||.(y1 - y2).|| )
assume ( y1 in the carrier of (RUSp2RNSp X) & y2 in the carrier of (RUSp2RNSp X) ) ; :: thesis: |.((g /. y1) - (g /. y2)).| <= r * ||.(y1 - y2).||
reconsider x1 = y1, x2 = y2 as Point of X ;
||.(y1 - y2).|| = ||.(x1 - x2).|| by RHS4, RHS6;
hence |.((g /. y1) - (g /. y2)).| <= r * ||.(y1 - y2).|| by A2, AS; :: thesis: verum

end;

hence g is_Lipschitzian_on the carrier of (RUSp2RNSp X) by A2, A11, AS; :: thesis: verum

end;

assume A11: g is_Lipschitzian_on the carrier of (RUSp2RNSp X) ; :: 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 (RUSp2RNSp X) st y1 in the carrier of (RUSp2RNSp X) & y2 in the carrier of (RUSp2RNSp X) 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 (RUSp2RNSp X) ;
||.(x1 - x2).|| = ||.(y1 - y2).|| by RHS4, RHS6;
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