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 A1: X c= dom f ; :: thesis: ( ( f is_upper_semicontinuous_on X & f is_lower_semicontinuous_on X ) iff f | X is continuous )

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

( ( 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 A1: X c= dom f ; :: thesis: ( ( f is_upper_semicontinuous_on X & f is_lower_semicontinuous_on X ) iff f | X is continuous )

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

proof

( f is_upper_semicontinuous_on X & f is_lower_semicontinuous_on X implies f | X is continuous )
assume A3:
f | X is continuous
; :: thesis: ( f is_upper_semicontinuous_on X & f is_lower_semicontinuous_on X )

A4: for x0 being Real st x0 in X holds

f | X is_lower_semicontinuous_in x0

f | X is_upper_semicontinuous_in x0

end;A4: for x0 being Real st x0 in X holds

f | X is_lower_semicontinuous_in x0

proof

for x0 being Real st x0 in X holds
let x0 be Real; :: thesis: ( x0 in X implies f | X is_lower_semicontinuous_in x0 )

assume x0 in X ; :: thesis: f | X is_lower_semicontinuous_in x0

then A5: x0 in dom (f | X) by A1, RELAT_1:57;

then f | X is_continuous_in x0 by A3, FCONT_1:def 2;

hence f | X is_lower_semicontinuous_in x0 by A5, Th21; :: thesis: verum

end;assume x0 in X ; :: thesis: f | X is_lower_semicontinuous_in x0

then A5: x0 in dom (f | X) by A1, RELAT_1:57;

then f | X is_continuous_in x0 by A3, FCONT_1:def 2;

hence f | X is_lower_semicontinuous_in x0 by A5, Th21; :: thesis: verum

f | X is_upper_semicontinuous_in x0

proof

hence
( f is_upper_semicontinuous_on X & f is_lower_semicontinuous_on X )
by A1, A4; :: thesis: verum
let x0 be Real; :: thesis: ( x0 in X implies f | X is_upper_semicontinuous_in x0 )

assume x0 in X ; :: thesis: f | X is_upper_semicontinuous_in x0

then A6: x0 in dom (f | X) by A1, RELAT_1:57;

then f | X is_continuous_in x0 by A3, FCONT_1:def 2;

hence f | X is_upper_semicontinuous_in x0 by A6, Th21; :: thesis: verum

end;assume x0 in X ; :: thesis: f | X is_upper_semicontinuous_in x0

then A6: x0 in dom (f | X) by A1, RELAT_1:57;

then f | X is_continuous_in x0 by A3, FCONT_1:def 2;

hence f | X is_upper_semicontinuous_in x0 by A6, Th21; :: thesis: verum

proof

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

A7: f is_upper_semicontinuous_on X and

A8: f is_lower_semicontinuous_on X ; :: thesis: f | X is continuous

( X c= dom f & ( for x0 being Real st x0 in dom (f | X) holds

f | X is_continuous_in x0 ) )

end;A7: f is_upper_semicontinuous_on X and

A8: f is_lower_semicontinuous_on X ; :: thesis: f | X is continuous

( X c= dom f & ( for x0 being Real st x0 in dom (f | X) holds

f | X is_continuous_in x0 ) )

proof

hence
f | X is continuous
by FCONT_1:def 2; :: thesis: verum
thus
X c= dom f
by A7; :: thesis: for x0 being Real st x0 in dom (f | X) holds

f | X is_continuous_in x0

let x0 be Real; :: thesis: ( x0 in dom (f | X) implies f | X is_continuous_in x0 )

assume A9: x0 in dom (f | X) ; :: thesis: f | X is_continuous_in x0

x0 in X by A9, RELAT_1:57;

then ( f | X is_upper_semicontinuous_in x0 & f | X is_lower_semicontinuous_in x0 ) by A7, A8;

hence f | X is_continuous_in x0 by Th21; :: thesis: verum

end;f | X is_continuous_in x0

let x0 be Real; :: thesis: ( x0 in dom (f | X) implies f | X is_continuous_in x0 )

assume A9: x0 in dom (f | X) ; :: thesis: f | X is_continuous_in x0

x0 in X by A9, RELAT_1:57;

then ( f | X is_upper_semicontinuous_in x0 & f | X is_lower_semicontinuous_in x0 ) by A7, A8;

hence f | X is_continuous_in x0 by Th21; :: thesis: verum