let X be set ; :: thesis: for f being PartFunc of COMPLEX,COMPLEX holds
( f is_continuous_on X iff f | X is_continuous_on X )
let f be PartFunc of COMPLEX,COMPLEX; :: thesis: ( f is_continuous_on X iff f | X is_continuous_on X )
thus ( f is_continuous_on X implies f | X is_continuous_on X ) :: thesis: ( f | X is_continuous_on X implies f is_continuous_on X )
proof
assume A1: f is_continuous_on X ; :: thesis: f | X is_continuous_on X
then X c= dom f ;
then X c= (dom f) /\ X by XBOOLE_1:28;
hence X c= dom (f | X) by RELAT_1:61; :: according to CFCONT_1:def 2 :: thesis: for x0 being Complex st x0 in X holds
(f | X) | X is_continuous_in x0
let g be Complex; :: thesis: ( g in X implies (f | X) | X is_continuous_in g )
assume g in X ; :: thesis: (f | X) | X is_continuous_in g
then f | X is_continuous_in g by A1;
hence (f | X) | X is_continuous_in g by RELAT_1:72; :: thesis: verum
end;
assume A2: f | X is_continuous_on X ; :: thesis: f is_continuous_on X
then X c= dom (f | X) ;
then ( (dom f) /\ X c= dom f & X c= (dom f) /\ X ) by RELAT_1:61, XBOOLE_1:17;
hence X c= dom f ; :: according to CFCONT_1:def 2 :: thesis: for x0 being Complex st x0 in X holds
f | X is_continuous_in x0
let g be Complex; :: thesis: ( g in X implies f | X is_continuous_in g )
assume g in X ; :: thesis: f | X is_continuous_in g
then (f | X) | X is_continuous_in g by A2;
hence f | X is_continuous_in g by RELAT_1:72; :: thesis: verum