let Y be RealNormSpace; :: thesis: for I being Function of REAL,()
for x0 being Point of ()
for y0 being Element of REAL
for g being PartFunc of REAL,Y
for f being PartFunc of (),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,(); :: thesis: for x0 being Point of ()
for y0 being Element of REAL
for g being PartFunc of REAL,Y
for f being PartFunc of (),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 (); :: thesis: for y0 being Element of REAL
for g being PartFunc of REAL,Y
for f being PartFunc of (),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 (),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 (),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 (),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 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
I /. y0 = x0 by ;
hence ( f is_continuous_in x0 implies g is_continuous_in y0 ) by ; :: thesis: verum
end;
A2: I * J = id () by ;
A3: g * J = f * (id ()) by
.= f by FUNCT_2:17 ;
J /. x0 = y0 by ;
hence ( g is_continuous_in y0 implies f is_continuous_in x0 ) by ; :: thesis: verum