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

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

let g be Function of (),REAL; :: thesis: ( f = g implies ( f is_continuous_on the carrier of X iff g is_continuous_on the carrier of () ) )
assume AS: f = g ; :: thesis: ( f is_continuous_on the carrier of X iff g is_continuous_on the carrier of () )
set Y = RUSp2RNSp X;
hereby :: thesis: ( g is_continuous_on the carrier of () implies f is_continuous_on the carrier of X )
assume A11: f is_continuous_on the carrier of X ; :: thesis: g is_continuous_on the carrier of ()
for y0 being Point of () st y0 in the carrier of () holds
g | the carrier of () is_continuous_in y0
proof
let y0 be Point of (); :: thesis: ( y0 in the carrier of () implies g | the carrier of () is_continuous_in y0 )
assume y0 in the carrier of () ; :: thesis: g | the carrier of () is_continuous_in y0
reconsider x0 = y0 as Point of X ;
f | the carrier of X is_continuous_in x0 by A11;
hence g | the carrier of () is_continuous_in y0 by ; :: thesis: verum
end;
hence g is_continuous_on the carrier of () by ; :: thesis: verum
end;
assume A31: g is_continuous_on the carrier of () ; :: thesis: f is_continuous_on the carrier of X
for x0 being Point of X st x0 in the carrier of X holds
f | the carrier of X is_continuous_in x0
proof
let x0 be Point of X; :: thesis: ( x0 in the carrier of X implies f | the carrier of X is_continuous_in x0 )
assume x0 in the carrier of X ; :: thesis: f | the carrier of X is_continuous_in x0
reconsider y0 = x0 as Point of () ;
g | the carrier of () is_continuous_in y0 by A31;
hence f | the carrier of X is_continuous_in x0 by ; :: thesis: verum
end;
hence f is_continuous_on the carrier of X by ; :: thesis: verum