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_continuous_on the carrier of X iff g is_continuous_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_continuous_on the carrier of X iff g is_continuous_on the carrier of (RUSp2RNSp X) )
let g be Function of (RUSp2RNSp X),REAL; :: thesis: ( f = g implies ( f is_continuous_on the carrier of X iff g is_continuous_on the carrier of (RUSp2RNSp X) ) )
assume AS: f = g ; :: thesis: ( f is_continuous_on the carrier of X iff g is_continuous_on the carrier of (RUSp2RNSp X) )
set Y = RUSp2RNSp X;
hereby :: thesis: ( g is_continuous_on the carrier of (RUSp2RNSp X) 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 (RUSp2RNSp X)
for y0 being Point of (RUSp2RNSp X) st y0 in the carrier of (RUSp2RNSp X) holds
g | the carrier of (RUSp2RNSp X) is_continuous_in y0
proof
let y0 be Point of (RUSp2RNSp X); :: thesis: ( y0 in the carrier of (RUSp2RNSp X) implies g | the carrier of (RUSp2RNSp X) is_continuous_in y0 )
assume y0 in the carrier of (RUSp2RNSp X) ; :: thesis: g | the carrier of (RUSp2RNSp X) 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 (RUSp2RNSp X) is_continuous_in y0 by LM3B, AS; :: thesis: verum
end;
hence g is_continuous_on the carrier of (RUSp2RNSp X) by A11, AS; :: thesis: verum
end;
assume A31: g is_continuous_on the carrier of (RUSp2RNSp X) ; :: 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 (RUSp2RNSp X) ;
g | the carrier of (RUSp2RNSp X) is_continuous_in y0 by A31;
hence f | the carrier of X is_continuous_in x0 by LM3B, AS; :: thesis: verum
end;
hence f is_continuous_on the carrier of X by A31, AS; :: thesis: verum