let X be RealUnitarySpace; :: thesis: for f being Function of X,REAL st f is_Lipschitzian_on the carrier of X holds
f is_continuous_on the carrier of X
let f be Function of X,REAL; :: thesis: ( f is_Lipschitzian_on the carrier of X implies f is_continuous_on the carrier of X )
assume AS: f is_Lipschitzian_on the carrier of X ; :: thesis: f is_continuous_on the carrier of X
reconsider g = f as Function of (RUSp2RNSp X),REAL ;
set Y = RUSp2RNSp X;
g is_Lipschitzian_on the carrier of (RUSp2RNSp X) by AS, LM4;
then g is_continuous_on the carrier of (RUSp2RNSp X) by NFCONT_1:46;
hence f is_continuous_on the carrier of X by LM3C; :: thesis: verum