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;

for x0 being Point of X st x0 in the carrier of X holds

f | the carrier of X is_continuous_in x0

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 A31:
g is_continuous_on the carrier of (RUSp2RNSp X)
; :: thesis: f is_continuous_on the carrier of Xassume 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

end;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

hence
g is_continuous_on the carrier of (RUSp2RNSp X)
by A11, AS; :: thesis: verum
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;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

for x0 being Point of X st x0 in the carrier of X holds

f | the carrier of X is_continuous_in x0

proof

hence
f is_continuous_on the carrier of X
by A31, AS; :: thesis: verum
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;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