let X be set ; :: thesis: for f being PartFunc of REAL ,REAL st X c= dom f holds
( ( f is_upper_semicontinuous_on X & f is_lower_semicontinuous_on X ) iff f | X is continuous )
let f be PartFunc of REAL ,REAL ; :: thesis: ( X c= dom f implies ( ( f is_upper_semicontinuous_on X & f is_lower_semicontinuous_on X ) iff f | X is continuous ) )
assume Z: X c= dom f ; :: thesis: ( ( f is_upper_semicontinuous_on X & f is_lower_semicontinuous_on X ) iff f | X is continuous )
A1: ( f is_upper_semicontinuous_on X & f is_lower_semicontinuous_on X implies f | X is continuous )

proof

assume A2: ( f is_upper_semicontinuous_on X & f is_lower_semicontinuous_on X ) ; :: thesis: f | X is continuous
( X c= dom f & ( for x0 being real number st x0 in dom (f | X) holds
f | X is_continuous_in x0 ) )

proof

thus X c= dom f by A2, Def6; :: thesis: for x0 being real number st x0 in dom (f | X) holds
f | X is_continuous_in x0
let x0 be real number ; :: thesis: ( x0 in dom (f | X) implies f | X is_continuous_in x0 )
assume X: x0 in dom (f | X) ; :: thesis: f | X is_continuous_in x0
A3: x0 in X by X, RELAT_1:86;
x0 is Real by XREAL_0:def 1;
then ( f | X is_upper_semicontinuous_in x0 & f | X is_lower_semicontinuous_in x0 ) by A2, A3, Def6, Def8;
hence f | X is_continuous_in x0 by Th20, X; :: thesis: verum

end;

hence f | X is continuous by FCONT_1:def 2; :: thesis: verum

end;

( f | X is continuous implies ( f is_upper_semicontinuous_on X & f is_lower_semicontinuous_on X ) )

proof

assume A4: f | X is continuous ; :: thesis: ( f is_upper_semicontinuous_on X & f is_lower_semicontinuous_on X )
( X c= dom f & ( for x0 being Real st x0 in X holds
f | X is_upper_semicontinuous_in x0 ) & ( for x0 being Real st x0 in X holds
f | X is_lower_semicontinuous_in x0 ) )

proof

thus K: X c= dom f by Z; :: thesis: ( ( for x0 being Real st x0 in X holds
f | X is_upper_semicontinuous_in x0 ) & ( for x0 being Real st x0 in X holds
f | X is_lower_semicontinuous_in x0 ) )
A5: for x0 being Real st x0 in X holds
f | X is_upper_semicontinuous_in x0

proof

let x0 be Real; :: thesis: ( x0 in X implies f | X is_upper_semicontinuous_in x0 )
assume A6: x0 in X ; :: thesis: f | X is_upper_semicontinuous_in x0
then x0 in dom f by K;
then X: x0 in dom (f | X) by A6, RELAT_1:86;
f | X is_upper_semicontinuous_in x0

proof

f | X is_continuous_in x0 by A4, X, FCONT_1:def 2;
hence f | X is_upper_semicontinuous_in x0 by Th20, X; :: thesis: verum

end;

hence f | X is_upper_semicontinuous_in x0 ; :: thesis: verum

end;

for x0 being Real st x0 in X holds
f | X is_lower_semicontinuous_in x0

proof

let x0 be Real; :: thesis: ( x0 in X implies f | X is_lower_semicontinuous_in x0 )
assume A7: x0 in X ; :: thesis: f | X is_lower_semicontinuous_in x0
then x0 in dom f by K;
then X: x0 in dom (f | X) by A7, RELAT_1:86;
f | X is_lower_semicontinuous_in x0

proof

f | X is_continuous_in x0 by A4, X, FCONT_1:def 2;
hence f | X is_lower_semicontinuous_in x0 by Th20, X; :: thesis: verum

end;

hence f | X is_lower_semicontinuous_in x0 ; :: thesis: verum

end;

hence ( ( for x0 being Real st x0 in X holds
f | X is_upper_semicontinuous_in x0 ) & ( for x0 being Real st x0 in X holds
f | X is_lower_semicontinuous_in x0 ) ) by A5; :: thesis: verum

end;

hence ( f is_upper_semicontinuous_on X & f is_lower_semicontinuous_on X ) by Def6, Def8; :: thesis: verum

end;

hence ( ( f is_upper_semicontinuous_on X & f is_lower_semicontinuous_on X ) iff f | X is continuous ) by A1; :: thesis: verum