let Y be RealNormSpace; :: thesis: 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,Y

for f being PartFunc of (REAL-NS 1),Y 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); :: 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 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); :: thesis: for y0 being Element of REAL

for g being PartFunc of REAL,Y

for f being PartFunc of (REAL-NS 1),Y 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 ; :: thesis: for g being PartFunc of REAL,Y

for f being PartFunc of (REAL-NS 1),Y 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,Y; :: thesis: for f being PartFunc of (REAL-NS 1),Y 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),Y; :: thesis: ( 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 ) ; :: thesis: ( 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 ) :: thesis: ( g is_continuous_in y0 implies f is_continuous_in x0 )

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, NDIFF_4:32, A1, 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 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); :: 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 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); :: thesis: for y0 being Element of REAL

for g being PartFunc of REAL,Y

for f being PartFunc of (REAL-NS 1),Y 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 ; :: thesis: for g being PartFunc of REAL,Y

for f being PartFunc of (REAL-NS 1),Y 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,Y; :: thesis: for f being PartFunc of (REAL-NS 1),Y 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),Y; :: thesis: ( 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 ) ; :: thesis: ( 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 ) :: thesis: ( g is_continuous_in y0 implies f is_continuous_in x0 )

proof

A2:
I * J = id (REAL-NS 1)
by A1, Lm2, Lm1, FUNCT_1:39;
I /. y0 = x0
by A1, PDIFF_1:1;

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

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

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, NDIFF_4:32, A1, NDIFF_4:34; :: thesis: verum