let Y be RealNormSpace; :: thesis: for J being Function of (REAL-NS 1),REAL

for x0 being Point of (REAL-NS 1)

for y0 being Element of REAL

for g being PartFunc of REAL,Y

for f being PartFunc of (REAL-NS 1),Y st J = proj (1,1) & x0 in dom f & y0 in dom g & x0 = <*y0*> & f = g * J holds

( f is_continuous_in x0 iff g is_continuous_in y0 )

let J be Function of (REAL-NS 1),REAL; :: thesis: for x0 being Point of (REAL-NS 1)

for y0 being Element of REAL

for g being PartFunc of REAL,Y

for f being PartFunc of (REAL-NS 1),Y st J = proj (1,1) & x0 in dom f & y0 in dom g & x0 = <*y0*> & f = g * J holds

( f is_continuous_in x0 iff g is_continuous_in y0 )

let x0 be Point of (REAL-NS 1); :: thesis: for y0 being Element of REAL

for g being PartFunc of REAL,Y

for f being PartFunc of (REAL-NS 1),Y st J = proj (1,1) & x0 in dom f & y0 in dom g & x0 = <*y0*> & f = g * J holds

( f is_continuous_in x0 iff g is_continuous_in y0 )

let y0 be Element of REAL ; :: thesis: for g being PartFunc of REAL,Y

for f being PartFunc of (REAL-NS 1),Y st J = proj (1,1) & x0 in dom f & y0 in dom g & x0 = <*y0*> & f = g * J holds

( f is_continuous_in x0 iff g is_continuous_in y0 )

let g be PartFunc of REAL,Y; :: thesis: for f being PartFunc of (REAL-NS 1),Y st J = proj (1,1) & x0 in dom f & y0 in dom g & x0 = <*y0*> & f = g * J holds

( f is_continuous_in x0 iff g is_continuous_in y0 )

let f be PartFunc of (REAL-NS 1),Y; :: thesis: ( J = proj (1,1) & x0 in dom f & y0 in dom g & x0 = <*y0*> & f = g * J implies ( f is_continuous_in x0 iff g is_continuous_in y0 ) )

assume A1: ( J = proj (1,1) & x0 in dom f & y0 in dom g & x0 = <*y0*> & f = g * J ) ; :: thesis: ( f is_continuous_in x0 iff g is_continuous_in y0 )

thus ( f is_continuous_in x0 implies g is_continuous_in y0 ) :: thesis: ( g is_continuous_in y0 implies f is_continuous_in x0 )

hence ( g is_continuous_in y0 implies f is_continuous_in x0 ) by A1, NDIFF_4:32, NDIFF_4:34; :: thesis: verum

for x0 being Point of (REAL-NS 1)

for y0 being Element of REAL

for g being PartFunc of REAL,Y

for f being PartFunc of (REAL-NS 1),Y st J = proj (1,1) & x0 in dom f & y0 in dom g & x0 = <*y0*> & f = g * J holds

( f is_continuous_in x0 iff g is_continuous_in y0 )

let J be Function of (REAL-NS 1),REAL; :: thesis: for x0 being Point of (REAL-NS 1)

for y0 being Element of REAL

for g being PartFunc of REAL,Y

for f being PartFunc of (REAL-NS 1),Y st J = proj (1,1) & x0 in dom f & y0 in dom g & x0 = <*y0*> & f = g * J holds

( f is_continuous_in x0 iff g is_continuous_in y0 )

let x0 be Point of (REAL-NS 1); :: thesis: for y0 being Element of REAL

for g being PartFunc of REAL,Y

for f being PartFunc of (REAL-NS 1),Y st J = proj (1,1) & x0 in dom f & y0 in dom g & x0 = <*y0*> & f = g * J holds

( f is_continuous_in x0 iff g is_continuous_in y0 )

let y0 be Element of REAL ; :: thesis: for g being PartFunc of REAL,Y

for f being PartFunc of (REAL-NS 1),Y st J = proj (1,1) & x0 in dom f & y0 in dom g & x0 = <*y0*> & f = g * J holds

( f is_continuous_in x0 iff g is_continuous_in y0 )

let g be PartFunc of REAL,Y; :: thesis: for f being PartFunc of (REAL-NS 1),Y st J = proj (1,1) & x0 in dom f & y0 in dom g & x0 = <*y0*> & f = g * J holds

( f is_continuous_in x0 iff g is_continuous_in y0 )

let f be PartFunc of (REAL-NS 1),Y; :: thesis: ( J = proj (1,1) & x0 in dom f & y0 in dom g & x0 = <*y0*> & f = g * J implies ( f is_continuous_in x0 iff g is_continuous_in y0 ) )

assume A1: ( J = proj (1,1) & x0 in dom f & y0 in dom g & x0 = <*y0*> & f = g * J ) ; :: thesis: ( f is_continuous_in x0 iff g is_continuous_in y0 )

thus ( f is_continuous_in x0 implies g is_continuous_in y0 ) :: thesis: ( g is_continuous_in y0 implies f is_continuous_in x0 )

proof

J /. x0 = y0
by A1, PDIFF_1:1;
reconsider I = (proj (1,1)) " as Function of REAL,(REAL-NS 1) by PDIFF_1:2, REAL_NS1:def 4;

A2: J * I = id REAL by A1, Lm2, FUNCT_1:39;

f * I = g * (id REAL) by A1, A2, RELAT_1:36;

then A3: f * I = g by FUNCT_2:17;

I /. y0 = x0 by A1, PDIFF_1:1;

hence ( f is_continuous_in x0 implies g is_continuous_in y0 ) by A3, NDIFF_4:33, A1, NFCONT_3:15; :: thesis: verum

end;A2: J * I = id REAL by A1, Lm2, FUNCT_1:39;

f * I = g * (id REAL) by A1, A2, RELAT_1:36;

then A3: f * I = g by FUNCT_2:17;

I /. y0 = x0 by A1, PDIFF_1:1;

hence ( f is_continuous_in x0 implies g is_continuous_in y0 ) by A3, NDIFF_4:33, A1, NFCONT_3:15; :: thesis: verum

hence ( g is_continuous_in y0 implies f is_continuous_in x0 ) by A1, NDIFF_4:32, NDIFF_4:34; :: thesis: verum