let CNS1, CNS2 be ComplexNormSpace; :: thesis: for X being set
for f being PartFunc of CNS1,CNS2 holds
( f is_continuous_on X iff f | X is_continuous_on X )
let X be set ; :: thesis: for f being PartFunc of CNS1,CNS2 holds
( f is_continuous_on X iff f | X is_continuous_on X )
let f be PartFunc of CNS1,CNS2; :: 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 NCFCONT1:def 11 :: thesis: for x0 being Point of CNS1 st x0 in X holds
(f | X) | X is_continuous_in x0
let r be Point of CNS1; :: thesis: ( r in X implies (f | X) | X is_continuous_in r )
assume r in X ; :: thesis: (f | X) | X is_continuous_in r
then f | X is_continuous_in r by A1;
hence (f | X) | X is_continuous_in r 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 NCFCONT1:def 11 :: thesis: for x0 being Point of CNS1 st x0 in X holds
f | X is_continuous_in x0
let r be Point of CNS1; :: thesis: ( r in X implies f | X is_continuous_in r )
assume r in X ; :: thesis: f | X is_continuous_in r
then (f | X) | X is_continuous_in r by A2;
hence f | X is_continuous_in r by RELAT_1:72; :: thesis: verum