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 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_differentiable_in x0 iff g is_differentiable_in y0 )

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

for y0 being 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_differentiable_in x0 iff g is_differentiable_in y0 )

let x0 be Point of (REAL-NS 1); :: thesis: for y0 being 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_differentiable_in x0 iff g is_differentiable_in y0 )

let y0 be 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_differentiable_in x0 iff g is_differentiable_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_differentiable_in x0 iff g is_differentiable_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_differentiable_in x0 iff g is_differentiable_in y0 ) )

assume that

A1: I = (proj (1,1)) " and

A2: x0 in dom f and

A3: y0 in dom g and

A4: x0 = <*y0*> and

A5: f * I = g ; :: thesis: ( f is_differentiable_in x0 iff g is_differentiable_in y0 )

reconsider J = proj (1,1) as Function of (REAL-NS 1),REAL by Lm1;

thus ( f is_differentiable_in x0 implies g is_differentiable_in y0 ) by A2, A3, A4, A5, FTh42, A1; :: thesis: ( g is_differentiable_in y0 implies f is_differentiable_in x0 )

assume g is_differentiable_in y0 ; :: thesis: f is_differentiable_in x0

then consider N0 being Neighbourhood of y0 such that

A6: N0 c= dom (f * I) and

A7: ex L being LinearFunc of Y ex R being RestFunc of Y st

for y being Real st y in N0 holds

((f * I) /. y) - ((f * I) /. y0) = (L /. (y - y0)) + (R /. (y - y0)) by A5;

reconsider y0 = y0 as Element of REAL by XREAL_0:def 1;

A8: I * J = id (REAL-NS 1) by Lm1, A1, Lm2, FUNCT_1:39;

A9: g * J = f * (id (REAL-NS 1)) by A5, A8, RELAT_1:36

.= f by FUNCT_2:17 ;

consider e0 being Real such that

A10: 0 < e0 and

A11: N0 = ].(y0 - e0),(y0 + e0).[ by RCOMP_1:def 6;

reconsider e = e0 as Element of REAL by XREAL_0:def 1;

set N = { z where z is Point of (REAL-NS 1) : ||.(z - x0).|| < e } ;

consider L being LinearFunc of Y, R being RestFunc of Y such that

A12: for y1 being Real st y1 in N0 holds

((f * I) /. y1) - ((f * I) /. y0) = (L /. (y1 - y0)) + (R /. (y1 - y0)) by A7;

reconsider R0 = R * J as RestFunc of (REAL-NS 1),Y by FTh41;

reconsider L0 = L * J as Lipschitzian LinearOperator of (REAL-NS 1),Y by FTh41;

I .: (dom g) = I .: (I " (dom f)) by A5, RELAT_1:147;

then A211: I .: (dom g) = dom f by A1, Lm1, FUNCT_1:77, PDIFF_1:2;

then A21: { z where z is Point of (REAL-NS 1) : ||.(z - x0).|| < e } c= dom f by A5, A6, A20, RELAT_1:123;

{ z where z is Point of (REAL-NS 1) : ||.(z - x0).|| < e } c= the carrier of (REAL-NS 1)

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

then (J * I) .: N0 = N0 by FRECHET:13;

then A23: J .: { z where z is Point of (REAL-NS 1) : ||.(z - x0).|| < e } = N0 by A20, RELAT_1:126;

A24: for y being Point of (REAL-NS 1) st y in { z where z is Point of (REAL-NS 1) : ||.(z - x0).|| < e } holds

(f /. y) - (f /. x0) = (L0 . (y - x0)) + (R0 /. (y - x0))

for x being Point of (REAL-NS 1) st x in { z where z is Point of (REAL-NS 1) : ||.(z - x0).|| < e } holds

(f /. x) - (f /. x0) = (L0 . (x - x0)) + (R0 /. (x - x0)) by A24;

hence f is_differentiable_in x0 by A22, A211, A5, A6, A20, RELAT_1:123; :: thesis: verum

for x0 being Point of (REAL-NS 1)

for y0 being 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_differentiable_in x0 iff g is_differentiable_in y0 )

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

for y0 being 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_differentiable_in x0 iff g is_differentiable_in y0 )

let x0 be Point of (REAL-NS 1); :: thesis: for y0 being 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_differentiable_in x0 iff g is_differentiable_in y0 )

let y0 be 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_differentiable_in x0 iff g is_differentiable_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_differentiable_in x0 iff g is_differentiable_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_differentiable_in x0 iff g is_differentiable_in y0 ) )

assume that

A1: I = (proj (1,1)) " and

A2: x0 in dom f and

A3: y0 in dom g and

A4: x0 = <*y0*> and

A5: f * I = g ; :: thesis: ( f is_differentiable_in x0 iff g is_differentiable_in y0 )

reconsider J = proj (1,1) as Function of (REAL-NS 1),REAL by Lm1;

thus ( f is_differentiable_in x0 implies g is_differentiable_in y0 ) by A2, A3, A4, A5, FTh42, A1; :: thesis: ( g is_differentiable_in y0 implies f is_differentiable_in x0 )

assume g is_differentiable_in y0 ; :: thesis: f is_differentiable_in x0

then consider N0 being Neighbourhood of y0 such that

A6: N0 c= dom (f * I) and

A7: ex L being LinearFunc of Y ex R being RestFunc of Y st

for y being Real st y in N0 holds

((f * I) /. y) - ((f * I) /. y0) = (L /. (y - y0)) + (R /. (y - y0)) by A5;

reconsider y0 = y0 as Element of REAL by XREAL_0:def 1;

A8: I * J = id (REAL-NS 1) by Lm1, A1, Lm2, FUNCT_1:39;

A9: g * J = f * (id (REAL-NS 1)) by A5, A8, RELAT_1:36

.= f by FUNCT_2:17 ;

consider e0 being Real such that

A10: 0 < e0 and

A11: N0 = ].(y0 - e0),(y0 + e0).[ by RCOMP_1:def 6;

reconsider e = e0 as Element of REAL by XREAL_0:def 1;

set N = { z where z is Point of (REAL-NS 1) : ||.(z - x0).|| < e } ;

consider L being LinearFunc of Y, R being RestFunc of Y such that

A12: for y1 being Real st y1 in N0 holds

((f * I) /. y1) - ((f * I) /. y0) = (L /. (y1 - y0)) + (R /. (y1 - y0)) by A7;

reconsider R0 = R * J as RestFunc of (REAL-NS 1),Y by FTh41;

reconsider L0 = L * J as Lipschitzian LinearOperator of (REAL-NS 1),Y by FTh41;

now :: thesis: for z being object holds

( ( z in { z where z is Point of (REAL-NS 1) : ||.(z - x0).|| < e } implies z in I .: N0 ) & ( z in I .: N0 implies z in { z where z is Point of (REAL-NS 1) : ||.(z - x0).|| < e } ) )

then A20:
{ z where z is Point of (REAL-NS 1) : ||.(z - x0).|| < e } = I .: N0
by TARSKI:2;( ( z in { z where z is Point of (REAL-NS 1) : ||.(z - x0).|| < e } implies z in I .: N0 ) & ( z in I .: N0 implies z in { z where z is Point of (REAL-NS 1) : ||.(z - x0).|| < e } ) )

let z be object ; :: thesis: ( ( z in { z where z is Point of (REAL-NS 1) : ||.(z - x0).|| < e } implies z in I .: N0 ) & ( z in I .: N0 implies z in { z where z is Point of (REAL-NS 1) : ||.(z - x0).|| < e } ) )

then consider yy being object such that

A16: yy in REAL and

A17: yy in N0 and

A18: z = I . yy by FUNCT_2:64;

reconsider y3 = yy as Element of REAL by A16;

set w = I . y3;

I . y0 = x0 by A4, A1, Lm2;

then A19: (I . y3) - x0 = I . (y3 - y0) by A1, Lm1, PDIFF_1:3;

|.(y3 - y0).| < e by A11, A17, RCOMP_1:1;

then ||.((I . y3) - x0).|| < e by A19, A1, Lm1, PDIFF_1:3;

hence z in { z where z is Point of (REAL-NS 1) : ||.(z - x0).|| < e } by A18; :: thesis: verum

end;hereby :: thesis: ( z in I .: N0 implies z in { z where z is Point of (REAL-NS 1) : ||.(z - x0).|| < e } )

assume
z in I .: N0
; :: thesis: z in { z where z is Point of (REAL-NS 1) : ||.(z - x0).|| < e } assume
z in { z where z is Point of (REAL-NS 1) : ||.(z - x0).|| < e }
; :: thesis: z in I .: N0

then consider w being Point of (REAL-NS 1) such that

A13: z = w and

A14: ||.(w - x0).|| < e ;

reconsider y2 = J . w as Element of REAL ;

J . x0 = y0 by A4, Lm2;

then J . (w - x0) = y2 - y0 by PDIFF_1:4;

then |.(y2 - y0).| < e by A14, PDIFF_1:4;

then A15: y2 in N0 by A11, RCOMP_1:1;

w in the carrier of (REAL-NS 1) ;

then w in dom J by Lm2, REAL_NS1:def 4;

then w = I . y2 by A1, FUNCT_1:34;

hence z in I .: N0 by A13, A15, FUNCT_2:35; :: thesis: verum

end;then consider w being Point of (REAL-NS 1) such that

A13: z = w and

A14: ||.(w - x0).|| < e ;

reconsider y2 = J . w as Element of REAL ;

J . x0 = y0 by A4, Lm2;

then J . (w - x0) = y2 - y0 by PDIFF_1:4;

then |.(y2 - y0).| < e by A14, PDIFF_1:4;

then A15: y2 in N0 by A11, RCOMP_1:1;

w in the carrier of (REAL-NS 1) ;

then w in dom J by Lm2, REAL_NS1:def 4;

then w = I . y2 by A1, FUNCT_1:34;

hence z in I .: N0 by A13, A15, FUNCT_2:35; :: thesis: verum

then consider yy being object such that

A16: yy in REAL and

A17: yy in N0 and

A18: z = I . yy by FUNCT_2:64;

reconsider y3 = yy as Element of REAL by A16;

set w = I . y3;

I . y0 = x0 by A4, A1, Lm2;

then A19: (I . y3) - x0 = I . (y3 - y0) by A1, Lm1, PDIFF_1:3;

|.(y3 - y0).| < e by A11, A17, RCOMP_1:1;

then ||.((I . y3) - x0).|| < e by A19, A1, Lm1, PDIFF_1:3;

hence z in { z where z is Point of (REAL-NS 1) : ||.(z - x0).|| < e } by A18; :: thesis: verum

I .: (dom g) = I .: (I " (dom f)) by A5, RELAT_1:147;

then A211: I .: (dom g) = dom f by A1, Lm1, FUNCT_1:77, PDIFF_1:2;

then A21: { z where z is Point of (REAL-NS 1) : ||.(z - x0).|| < e } c= dom f by A5, A6, A20, RELAT_1:123;

{ z where z is Point of (REAL-NS 1) : ||.(z - x0).|| < e } c= the carrier of (REAL-NS 1)

proof

then A22:
{ z where z is Point of (REAL-NS 1) : ||.(z - x0).|| < e } is Neighbourhood of x0
by A10, NFCONT_1:def 1;
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in { z where z is Point of (REAL-NS 1) : ||.(z - x0).|| < e } or y in the carrier of (REAL-NS 1) )

assume y in { z where z is Point of (REAL-NS 1) : ||.(z - x0).|| < e } ; :: thesis: y in the carrier of (REAL-NS 1)

then ex z being Point of (REAL-NS 1) st

( y = z & ||.(z - x0).|| < e ) ;

hence y in the carrier of (REAL-NS 1) ; :: thesis: verum

end;assume y in { z where z is Point of (REAL-NS 1) : ||.(z - x0).|| < e } ; :: thesis: y in the carrier of (REAL-NS 1)

then ex z being Point of (REAL-NS 1) st

( y = z & ||.(z - x0).|| < e ) ;

hence y in the carrier of (REAL-NS 1) ; :: thesis: verum

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

then (J * I) .: N0 = N0 by FRECHET:13;

then A23: J .: { z where z is Point of (REAL-NS 1) : ||.(z - x0).|| < e } = N0 by A20, RELAT_1:126;

A24: for y being Point of (REAL-NS 1) st y in { z where z is Point of (REAL-NS 1) : ||.(z - x0).|| < e } holds

(f /. y) - (f /. x0) = (L0 . (y - x0)) + (R0 /. (y - x0))

proof

reconsider L0 = L0 as Point of (R_NormSpace_of_BoundedLinearOperators ((REAL-NS 1),Y)) by LOPBAN_1:def 9;
x0 in the carrier of (REAL-NS 1)
;

then x0 in dom J by Lm2, REAL_NS1:def 4;

then g . (J . x0) = f . x0 by A9, FUNCT_1:13;

then A25: g . (J . x0) = f /. x0 by A2, PARTFUN1:def 6;

A26: J . x0 = y0 by A4, Lm2;

let y be Point of (REAL-NS 1); :: thesis: ( y in { z where z is Point of (REAL-NS 1) : ||.(z - x0).|| < e } implies (f /. y) - (f /. x0) = (L0 . (y - x0)) + (R0 /. (y - x0)) )

assume A27: y in { z where z is Point of (REAL-NS 1) : ||.(z - x0).|| < e } ; :: thesis: (f /. y) - (f /. x0) = (L0 . (y - x0)) + (R0 /. (y - x0))

set y3 = J . y;

reconsider p1 = g /. (J . y), p2 = g /. y0, q1 = L /. ((J . y) - y0), q2 = R /. ((J . y) - y0) as VECTOR of Y ;

A28: J . x0 = y0 by A4, Lm2;

(g /. (J . y)) - (g /. y0) = q1 + q2 by A5, A12, A23, A27, FUNCT_2:35;

then (g /. (J . y)) - (g /. (J . x0)) = (L /. (J . (y - x0))) + (R /. ((J . y) - y0)) by A28, PDIFF_1:4;

then A29: (g /. (J . y)) - (g /. (J . x0)) = (L /. (J . (y - x0))) + (R /. (J . (y - x0))) by A28, PDIFF_1:4;

A30: dom L0 = the carrier of (REAL-NS 1) by FUNCT_2:def 1;

y - x0 in the carrier of (REAL-NS 1) ;

then y - x0 in dom J by Lm2, REAL_NS1:def 4;

then A31: R . (J . (y - x0)) = (R * J) . (y - x0) by FUNCT_1:13;

R0 is total by NDIFF_1:def 5;

then A32: dom (R * J) = the carrier of (REAL-NS 1) by PARTFUN1:def 2;

A33: R . (J . (y - x0)) = R0 /. (y - x0) by A31, A32, PARTFUN1:def 6;

J . (y - x0) in dom R by A32, FUNCT_1:11;

then A34: R /. (J . (y - x0)) = R0 /. (y - x0) by A33, PARTFUN1:def 6;

y in the carrier of (REAL-NS 1) ;

then A35: y in dom J by Lm2, REAL_NS1:def 4;

g . (J . y) = f . y by A9, A35, FUNCT_1:13;

then A36: g . (J . y) = f /. y by A21, A27, PARTFUN1:def 6;

J . y in dom g by A21, A27, A9, FUNCT_1:11;

then g /. (J . y) = f /. y by A36, PARTFUN1:def 6;

then (g /. (J . y)) - (g /. (J . x0)) = (f /. y) - (f /. x0) by A3, A26, A25, PARTFUN1:def 6;

hence (f /. y) - (f /. x0) = (L0 . (y - x0)) + (R0 /. (y - x0)) by A29, A34, A30, FUNCT_1:12; :: thesis: verum

end;then x0 in dom J by Lm2, REAL_NS1:def 4;

then g . (J . x0) = f . x0 by A9, FUNCT_1:13;

then A25: g . (J . x0) = f /. x0 by A2, PARTFUN1:def 6;

A26: J . x0 = y0 by A4, Lm2;

let y be Point of (REAL-NS 1); :: thesis: ( y in { z where z is Point of (REAL-NS 1) : ||.(z - x0).|| < e } implies (f /. y) - (f /. x0) = (L0 . (y - x0)) + (R0 /. (y - x0)) )

assume A27: y in { z where z is Point of (REAL-NS 1) : ||.(z - x0).|| < e } ; :: thesis: (f /. y) - (f /. x0) = (L0 . (y - x0)) + (R0 /. (y - x0))

set y3 = J . y;

reconsider p1 = g /. (J . y), p2 = g /. y0, q1 = L /. ((J . y) - y0), q2 = R /. ((J . y) - y0) as VECTOR of Y ;

A28: J . x0 = y0 by A4, Lm2;

(g /. (J . y)) - (g /. y0) = q1 + q2 by A5, A12, A23, A27, FUNCT_2:35;

then (g /. (J . y)) - (g /. (J . x0)) = (L /. (J . (y - x0))) + (R /. ((J . y) - y0)) by A28, PDIFF_1:4;

then A29: (g /. (J . y)) - (g /. (J . x0)) = (L /. (J . (y - x0))) + (R /. (J . (y - x0))) by A28, PDIFF_1:4;

A30: dom L0 = the carrier of (REAL-NS 1) by FUNCT_2:def 1;

y - x0 in the carrier of (REAL-NS 1) ;

then y - x0 in dom J by Lm2, REAL_NS1:def 4;

then A31: R . (J . (y - x0)) = (R * J) . (y - x0) by FUNCT_1:13;

R0 is total by NDIFF_1:def 5;

then A32: dom (R * J) = the carrier of (REAL-NS 1) by PARTFUN1:def 2;

A33: R . (J . (y - x0)) = R0 /. (y - x0) by A31, A32, PARTFUN1:def 6;

J . (y - x0) in dom R by A32, FUNCT_1:11;

then A34: R /. (J . (y - x0)) = R0 /. (y - x0) by A33, PARTFUN1:def 6;

y in the carrier of (REAL-NS 1) ;

then A35: y in dom J by Lm2, REAL_NS1:def 4;

g . (J . y) = f . y by A9, A35, FUNCT_1:13;

then A36: g . (J . y) = f /. y by A21, A27, PARTFUN1:def 6;

J . y in dom g by A21, A27, A9, FUNCT_1:11;

then g /. (J . y) = f /. y by A36, PARTFUN1:def 6;

then (g /. (J . y)) - (g /. (J . x0)) = (f /. y) - (f /. x0) by A3, A26, A25, PARTFUN1:def 6;

hence (f /. y) - (f /. x0) = (L0 . (y - x0)) + (R0 /. (y - x0)) by A29, A34, A30, FUNCT_1:12; :: thesis: verum

for x being Point of (REAL-NS 1) st x in { z where z is Point of (REAL-NS 1) : ||.(z - x0).|| < e } holds

(f /. x) - (f /. x0) = (L0 . (x - x0)) + (R0 /. (x - x0)) by A24;

hence f is_differentiable_in x0 by A22, A211, A5, A6, A20, RELAT_1:123; :: thesis: verum