let n be non zero Element of NAT ; for I being Function of REAL,(REAL-NS 1)
for x0 being Point of (REAL-NS 1)
for y0 being Element of REAL
for g being PartFunc of REAL,(REAL-NS n)
for f being PartFunc of (REAL-NS 1),(REAL-NS n) st I = (proj (1,1)) " & x0 in dom f & y0 in dom g & x0 = <*y0*> & f * I = g holds
( f is_continuous_in x0 iff g is_continuous_in y0 )
let I be Function of REAL,(REAL-NS 1); for x0 being Point of (REAL-NS 1)
for y0 being Element of REAL
for g being PartFunc of REAL,(REAL-NS n)
for f being PartFunc of (REAL-NS 1),(REAL-NS n) st I = (proj (1,1)) " & x0 in dom f & y0 in dom g & x0 = <*y0*> & f * I = g holds
( f is_continuous_in x0 iff g is_continuous_in y0 )
let x0 be Point of (REAL-NS 1); for y0 being Element of REAL
for g being PartFunc of REAL,(REAL-NS n)
for f being PartFunc of (REAL-NS 1),(REAL-NS n) st I = (proj (1,1)) " & x0 in dom f & y0 in dom g & x0 = <*y0*> & f * I = g holds
( f is_continuous_in x0 iff g is_continuous_in y0 )
let y0 be Element of REAL ; for g being PartFunc of REAL,(REAL-NS n)
for f being PartFunc of (REAL-NS 1),(REAL-NS n) st I = (proj (1,1)) " & x0 in dom f & y0 in dom g & x0 = <*y0*> & f * I = g holds
( f is_continuous_in x0 iff g is_continuous_in y0 )
let g be PartFunc of REAL,(REAL-NS n); for f being PartFunc of (REAL-NS 1),(REAL-NS n) st I = (proj (1,1)) " & x0 in dom f & y0 in dom g & x0 = <*y0*> & f * I = g holds
( f is_continuous_in x0 iff g is_continuous_in y0 )
let f be PartFunc of (REAL-NS 1),(REAL-NS n); ( I = (proj (1,1)) " & x0 in dom f & y0 in dom g & x0 = <*y0*> & f * I = g implies ( f is_continuous_in x0 iff g is_continuous_in y0 ) )
assume A1:
( I = (proj (1,1)) " & x0 in dom f & y0 in dom g & x0 = <*y0*> & f * I = g )
; ( f is_continuous_in x0 iff g is_continuous_in y0 )
reconsider J = proj (1,1) as Function of (REAL-NS 1),REAL by Lm1;
thus
( f is_continuous_in x0 implies g is_continuous_in y0 )
( g is_continuous_in y0 implies f is_continuous_in x0 )
A2:
I * J = id (REAL-NS 1)
by A1, Lm2, Lm1, FUNCT_1:39;
A3: g * J =
f * (id (REAL-NS 1))
by A2, A1, RELAT_1:36
.=
f
by FUNCT_2:17
;
J /. x0 = y0
by A1, PDIFF_1:1;
hence
( g is_continuous_in y0 implies f is_continuous_in x0 )
by A3, Th32, A1, Th34; verum