let Y be RealNormSpace; 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_differentiable_in x0 iff g is_differentiable_in y0 )
let J be 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_differentiable_in x0 iff g is_differentiable_in y0 )
let x0 be 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_differentiable_in x0 iff g is_differentiable_in y0 )
let y0 be 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_differentiable_in x0 iff g is_differentiable_in y0 )
let g be 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_differentiable_in x0 iff g is_differentiable_in y0 )
let f be PartFunc of (REAL-NS 1),Y; ( 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 )
; ( f is_differentiable_in x0 iff g is_differentiable_in y0 )
reconsider I = (proj (1,1)) " as Function of REAL,(REAL-NS 1) by PDIFF_1:2, REAL_NS1:def 4;
J * I = id REAL
by A1, Lm2, FUNCT_1:39;
then f * I =
g * (id REAL)
by A1, RELAT_1:36
.=
g
by FUNCT_2:17
;
hence
( f is_differentiable_in x0 iff g is_differentiable_in y0 )
by A1, FTh43; verum