let n be non zero Element of NAT ; :: thesis: for J being Function of (),REAL
for x0 being Point of ()
for y0 being Element of REAL
for g being PartFunc of REAL,()
for f being PartFunc of (),() st J = proj (1,1) & x0 in dom f & y0 in dom g & x0 = <*y0*> & f = g * J holds
( f is_differentiable_in x0 iff g is_differentiable_in y0 )

let J be Function of (),REAL; :: thesis: for x0 being Point of ()
for y0 being Element of REAL
for g being PartFunc of REAL,()
for f being PartFunc of (),() st J = proj (1,1) & x0 in dom f & y0 in dom g & x0 = <*y0*> & f = g * J holds
( f is_differentiable_in x0 iff g is_differentiable_in y0 )

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

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

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

let f be PartFunc of (),(); :: thesis: ( J = proj (1,1) & x0 in dom f & y0 in dom g & x0 = <*y0*> & f = g * J implies ( f is_differentiable_in x0 iff g is_differentiable_in y0 ) )
assume A1: ( J = proj (1,1) & x0 in dom f & y0 in dom g & x0 = <*y0*> & f = g * J ) ; :: thesis: ( f is_differentiable_in x0 iff g is_differentiable_in y0 )
reconsider I = (proj (1,1)) " as Function of REAL,() by ;
A2: J * I = id REAL by ;
f * I = g * () by
.= g by FUNCT_2:17 ;
hence ( f is_differentiable_in x0 iff g is_differentiable_in y0 ) by ; :: thesis: verum