theorem :: CONVFUN1:6

for f being PartFunc of REAL,REAL
for g being Function of the carrier of RLS_Real,ExtREAL
for X being Subset of RLS_Real st X c= dom f & ( for x being Real holds
( ( x in X implies g . x = f . x ) & ( not x in X implies g . x = +infty ) ) ) holds
( g is convex iff ( f is_convex_on X & X is convex ) )