let n be Element of NAT ; :: thesis: for X being set
for x0 being Real
for f being PartFunc of REAL,(REAL n) st x0 in X & f is_continuous_in x0 holds
f | X is_continuous_in x0
let X be set ; :: thesis: for x0 being Real
for f being PartFunc of REAL,(REAL n) st x0 in X & f is_continuous_in x0 holds
f | X is_continuous_in x0
let x0 be Real; :: thesis: for f being PartFunc of REAL,(REAL n) st x0 in X & f is_continuous_in x0 holds
f | X is_continuous_in x0
let f be PartFunc of REAL,(REAL n); :: thesis: ( x0 in X & f is_continuous_in x0 implies f | X is_continuous_in x0 )
assume that
A1: x0 in X and
A2: f is_continuous_in x0 ; :: thesis: f | X is_continuous_in x0
consider g being PartFunc of REAL,(REAL-NS n) such that
A3: ( f = g & g is_continuous_in x0 ) by A2;
g | X is_continuous_in x0 by A1, A3, NFCONT_3:6;
hence f | X is_continuous_in x0 by A3; :: thesis: verum