let f be PartFunc of (REAL-NS 1),(REAL-NS 1); :: thesis: for g being PartFunc of REAL,REAL

for x being Point of (REAL-NS 1)

for y being Real st f = <>* g & x = <*y*> & g is_differentiable_in y holds

( f is_differentiable_in x & (diff (f,x)) . <*1*> = <*(diff (g,y))*> )

let g be PartFunc of REAL,REAL; :: thesis: for x being Point of (REAL-NS 1)

for y being Real st f = <>* g & x = <*y*> & g is_differentiable_in y holds

( f is_differentiable_in x & (diff (f,x)) . <*1*> = <*(diff (g,y))*> )

let x be Point of (REAL-NS 1); :: thesis: for y being Real st f = <>* g & x = <*y*> & g is_differentiable_in y holds

( f is_differentiable_in x & (diff (f,x)) . <*1*> = <*(diff (g,y))*> )

let y be Real; :: thesis: ( f = <>* g & x = <*y*> & g is_differentiable_in y implies ( f is_differentiable_in x & (diff (f,x)) . <*1*> = <*(diff (g,y))*> ) )

set J = proj (1,1);

assume that

A1: f = <>* g and

A2: x = <*y*> and

A3: g is_differentiable_in y ; :: thesis: ( f is_differentiable_in x & (diff (f,x)) . <*1*> = <*(diff (g,y))*> )

reconsider x0 = y as Real ;

consider N0 being Neighbourhood of x0 such that

A4: N0 c= dom g and

A5: ex L0 being LinearFunc ex R0 being RestFunc st

( diff (g,x0) = L0 . 1 & ( for y0 being Real st y0 in N0 holds

(g . y0) - (g . x0) = (L0 . (y0 - x0)) + (R0 . (y0 - x0)) ) ) by A3, FDIFF_1:def 5;

consider e0 being Real such that

A6: 0 < e0 and

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

reconsider e = e0 as Real ;

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

A8: rng (g * (proj (1,1))) c= REAL ;

consider L0 being LinearFunc, R0 being RestFunc such that

A9: diff (g,x0) = L0 . 1 and

A10: for y0 being Real st y0 in N0 holds

(g . y0) - (g . x0) = (L0 . (y0 - x0)) + (R0 . (y0 - x0)) by A5;

reconsider R = (I * R0) * (proj (1,1)) as RestFunc of (REAL-NS 1),(REAL-NS 1) by Th6;

reconsider L = (I * L0) * (proj (1,1)) as Lipschitzian LinearOperator of (REAL-NS 1),(REAL-NS 1) by Th6;

A11: dom g c= REAL ;

dom f c= the carrier of (REAL-NS 1) ;

then A12: dom f c= rng I by Th2, REAL_NS1:def 4;

A13: (proj (1,1)) * I = id REAL by Lm1, FUNCT_1:39;

(proj (1,1)) * f = (proj (1,1)) * (I * (g * (proj (1,1)))) by A1, RELAT_1:36;

then (proj (1,1)) * f = (id REAL) * (g * (proj (1,1))) by A13, RELAT_1:36;

then ((proj (1,1)) * f) * I = (g * (proj (1,1))) * I by A8, RELAT_1:53;

then ((proj (1,1)) * f) * I = g * (id REAL) by A13, RELAT_1:36;

then g = ((proj (1,1)) * f) * I by A11, RELAT_1:51;

then A22: dom g = I " (dom ((proj (1,1)) * f)) by RELAT_1:147;

rng f c= the carrier of (REAL-NS 1) ;

then rng f c= dom (proj (1,1)) by Lm1, REAL_NS1:def 4;

then I .: (dom g) = I .: (I " (dom f)) by A22, RELAT_1:27;

then I .: (dom g) = dom f by A12, FUNCT_1:77;

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

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

(proj (1,1)) * I = id REAL by Lm1, FUNCT_1:39;

then ((proj (1,1)) * I) .: N0 = N0 by FRECHET:13;

then A25: (proj (1,1)) .: { z where z is Point of (REAL-NS 1) : ||.(z - x).|| < e } = N0 by A21, RELAT_1:126;

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

(f /. y) - (f /. x) = (L . (y - x)) + (R /. (y - x))

then A40: dom L0 = REAL by PARTFUN1:def 2;

A41: L is Point of (R_NormSpace_of_BoundedLinearOperators ((REAL-NS 1),(REAL-NS 1))) by LOPBAN_1:def 9;

then f is_differentiable_in x by A24, A23, A26, NDIFF_1:def 6;

then diff (f,x) = (I * L0) * (proj (1,1)) by A24, A23, A41, A26, NDIFF_1:def 7;

then (diff (f,x)) . <*1*> = ((I * L0) * (proj (1,1))) . (I . 1) by Lm1;

then (diff (f,x)) . <*jj*> = (I * L0) . ((proj (1,1)) . (I . jj)) by Lm1, FUNCT_1:13;

then (diff (f,x)) . <*jj*> = I . (L0 . ((proj (1,1)) . (I . jj))) by A40, FUNCT_1:13;

then (diff (f,x)) . <*1*> = I . (L0 . 1) by Lm1, FUNCT_1:35;

hence ( f is_differentiable_in x & (diff (f,x)) . <*1*> = <*(diff (g,y))*> ) by A24, A23, A9, A41, A26, Lm1, NDIFF_1:def 6; :: thesis: verum

for x being Point of (REAL-NS 1)

for y being Real st f = <>* g & x = <*y*> & g is_differentiable_in y holds

( f is_differentiable_in x & (diff (f,x)) . <*1*> = <*(diff (g,y))*> )

let g be PartFunc of REAL,REAL; :: thesis: for x being Point of (REAL-NS 1)

for y being Real st f = <>* g & x = <*y*> & g is_differentiable_in y holds

( f is_differentiable_in x & (diff (f,x)) . <*1*> = <*(diff (g,y))*> )

let x be Point of (REAL-NS 1); :: thesis: for y being Real st f = <>* g & x = <*y*> & g is_differentiable_in y holds

( f is_differentiable_in x & (diff (f,x)) . <*1*> = <*(diff (g,y))*> )

let y be Real; :: thesis: ( f = <>* g & x = <*y*> & g is_differentiable_in y implies ( f is_differentiable_in x & (diff (f,x)) . <*1*> = <*(diff (g,y))*> ) )

set J = proj (1,1);

assume that

A1: f = <>* g and

A2: x = <*y*> and

A3: g is_differentiable_in y ; :: thesis: ( f is_differentiable_in x & (diff (f,x)) . <*1*> = <*(diff (g,y))*> )

reconsider x0 = y as Real ;

consider N0 being Neighbourhood of x0 such that

A4: N0 c= dom g and

A5: ex L0 being LinearFunc ex R0 being RestFunc st

( diff (g,x0) = L0 . 1 & ( for y0 being Real st y0 in N0 holds

(g . y0) - (g . x0) = (L0 . (y0 - x0)) + (R0 . (y0 - x0)) ) ) by A3, FDIFF_1:def 5;

consider e0 being Real such that

A6: 0 < e0 and

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

reconsider e = e0 as Real ;

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

A8: rng (g * (proj (1,1))) c= REAL ;

consider L0 being LinearFunc, R0 being RestFunc such that

A9: diff (g,x0) = L0 . 1 and

A10: for y0 being Real st y0 in N0 holds

(g . y0) - (g . x0) = (L0 . (y0 - x0)) + (R0 . (y0 - x0)) by A5;

reconsider R = (I * R0) * (proj (1,1)) as RestFunc of (REAL-NS 1),(REAL-NS 1) by Th6;

reconsider L = (I * L0) * (proj (1,1)) as Lipschitzian LinearOperator of (REAL-NS 1),(REAL-NS 1) by Th6;

A11: dom g c= REAL ;

dom f c= the carrier of (REAL-NS 1) ;

then A12: dom f c= rng I by Th2, REAL_NS1:def 4;

A13: (proj (1,1)) * I = id REAL by Lm1, FUNCT_1:39;

now :: thesis: for z being object holds

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

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

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

then consider yy being object such that

A17: yy in REAL and

A18: yy in N0 and

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

reconsider y = yy as Element of REAL by A17;

reconsider w = I . y as Point of (REAL-NS 1) by REAL_NS1:def 4;

I . x0 = x by A2, Lm1;

then A20: w - x = I . (y - x0) by Th3;

|.(y - x0).| < e by A7, A18, RCOMP_1:1;

then ||.(w - x).|| < e by A20, Th3;

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

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

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

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

A14: z = w and

A15: ||.(w - x).|| < e ;

reconsider y = (proj (1,1)) . w as Element of REAL by XREAL_0:def 1;

(proj (1,1)) . x = x0 by A2, Lm1;

then (proj (1,1)) . (w - x) = y - x0 by Th4;

then |.(y - x0).| < e by A15, Th4;

then A16: y in N0 by A7, RCOMP_1:1;

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

then w in dom (proj (1,1)) by Lm1, REAL_NS1:def 4;

then w = I . y by FUNCT_1:34;

hence z in I .: N0 by A14, A16, FUNCT_2:35; :: thesis: verum

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

A14: z = w and

A15: ||.(w - x).|| < e ;

reconsider y = (proj (1,1)) . w as Element of REAL by XREAL_0:def 1;

(proj (1,1)) . x = x0 by A2, Lm1;

then (proj (1,1)) . (w - x) = y - x0 by Th4;

then |.(y - x0).| < e by A15, Th4;

then A16: y in N0 by A7, RCOMP_1:1;

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

then w in dom (proj (1,1)) by Lm1, REAL_NS1:def 4;

then w = I . y by FUNCT_1:34;

hence z in I .: N0 by A14, A16, FUNCT_2:35; :: thesis: verum

then consider yy being object such that

A17: yy in REAL and

A18: yy in N0 and

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

reconsider y = yy as Element of REAL by A17;

reconsider w = I . y as Point of (REAL-NS 1) by REAL_NS1:def 4;

I . x0 = x by A2, Lm1;

then A20: w - x = I . (y - x0) by Th3;

|.(y - x0).| < e by A7, A18, RCOMP_1:1;

then ||.(w - x).|| < e by A20, Th3;

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

(proj (1,1)) * f = (proj (1,1)) * (I * (g * (proj (1,1)))) by A1, RELAT_1:36;

then (proj (1,1)) * f = (id REAL) * (g * (proj (1,1))) by A13, RELAT_1:36;

then ((proj (1,1)) * f) * I = (g * (proj (1,1))) * I by A8, RELAT_1:53;

then ((proj (1,1)) * f) * I = g * (id REAL) by A13, RELAT_1:36;

then g = ((proj (1,1)) * f) * I by A11, RELAT_1:51;

then A22: dom g = I " (dom ((proj (1,1)) * f)) by RELAT_1:147;

rng f c= the carrier of (REAL-NS 1) ;

then rng f c= dom (proj (1,1)) by Lm1, REAL_NS1:def 4;

then I .: (dom g) = I .: (I " (dom f)) by A22, RELAT_1:27;

then I .: (dom g) = dom f by A12, FUNCT_1:77;

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

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

proof

then A24:
{ z where z is Point of (REAL-NS 1) : ||.(z - x).|| < e } is Neighbourhood of x
by A6, 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 - x).|| < e } or y in the carrier of (REAL-NS 1) )

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

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

( y = z & ||.(z - x).|| < 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 - x).|| < e } ; :: thesis: y in the carrier of (REAL-NS 1)

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

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

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

(proj (1,1)) * I = id REAL by Lm1, FUNCT_1:39;

then ((proj (1,1)) * I) .: N0 = N0 by FRECHET:13;

then A25: (proj (1,1)) .: { z where z is Point of (REAL-NS 1) : ||.(z - x).|| < e } = N0 by A21, RELAT_1:126;

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

(f /. y) - (f /. x) = (L . (y - x)) + (R /. (y - x))

proof

L0 is total
by FDIFF_1:def 3;
x in the carrier of (REAL-NS 1)
;

then x in dom (proj (1,1)) by Lm1, REAL_NS1:def 4;

then A27: I . (g . ((proj (1,1)) . x)) = I . ((g * (proj (1,1))) . x) by FUNCT_1:13;

A28: x in { z where z is Point of (REAL-NS 1) : ||.(z - x).|| < e } by A24, NFCONT_1:4;

then x in dom f by A23;

then x in dom (I * (g * (proj (1,1)))) by A1, RELAT_1:36;

then I . (g . ((proj (1,1)) . x)) = (I * (g * (proj (1,1)))) . x by A27, FUNCT_1:12;

then I . (g . ((proj (1,1)) . x)) = f . x by A1, RELAT_1:36;

then A29: I . (g . ((proj (1,1)) . x)) = f /. x by A23, A28, PARTFUN1:def 6;

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

assume A30: y in { z where z is Point of (REAL-NS 1) : ||.(z - x).|| < e } ; :: thesis: (f /. y) - (f /. x) = (L . (y - x)) + (R /. (y - x))

reconsider y0 = (proj (1,1)) . y as Element of REAL by XREAL_0:def 1;

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

reconsider gy0 = g . y0, gx0 = g . x0, g0 = g . 0 as Element of REAL by XREAL_0:def 1;

reconsider L0y0x0 = L0 . y0x0 as Element of REAL by XREAL_0:def 1;

reconsider R0y0x0 = R0 . y0x0, Jyx = (proj (1,1)) . (y - x) as Element of REAL by XREAL_0:def 1;

reconsider gJy = g . ((proj (1,1)) . y), gJx = g . ((proj (1,1)) . x) as Element of REAL by XREAL_0:def 1;

reconsider R0Jyx = R0 . Jyx, L0Jyx = L0 . Jyx as Element of REAL by XREAL_0:def 1;

reconsider p1 = I . gy0, p2 = I . gx0, q1 = I . L0y0x0, q2 = I . R0y0x0 as VECTOR of (REAL-NS 1) by REAL_NS1:def 4;

A31: (proj (1,1)) . x = x0 by A2, Lm1;

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

then y in REAL 1 by REAL_NS1:def 4;

then I . ((g . y0) - (g . x0)) = I . ((L0 . (y0 - x0)) + (R0 . (y0 - x0))) by A10, A25, A30, FUNCT_2:35;

then p1 - p2 = I . ((L0 . (y0 - x0)) + (R0 . (y0 - x0))) by Th3;

then p1 - p2 = q1 + q2 by Th3;

then (I . gy0) - (I . gx0) = q1 + q2 by REAL_NS1:5;

then (I . gJy) - (I . gJx) = (I . L0y0x0) + (I . R0y0x0) by A31, REAL_NS1:2;

then (I . gJy) - (I . gJx) = (I . L0Jyx) + (I . R0y0x0) by A31, Th4;

then A32: (I . gJy) - (I . gJx) = (I . L0Jyx) + (I . R0Jyx) by A31, Th4;

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

then y - x in dom ((I * L0) * (proj (1,1))) ;

then A33: y - x in dom (I * (L0 * (proj (1,1)))) by RELAT_1:36;

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

then A34: y - x in dom (proj (1,1)) by Lm1, REAL_NS1:def 4;

then A35: I . (R0 . ((proj (1,1)) . (y - x))) = I . ((R0 * (proj (1,1))) . (y - x)) by FUNCT_1:13;

R is total by NDIFF_1:def 5;

then A36: dom ((I * R0) * (proj (1,1))) = the carrier of (REAL-NS 1) by PARTFUN1:def 2;

then y - x in dom ((I * R0) * (proj (1,1))) ;

then y - x in dom (I * (R0 * (proj (1,1)))) by RELAT_1:36;

then I . (R0 . ((proj (1,1)) . (y - x))) = (I * (R0 * (proj (1,1)))) . (y - x) by A35, FUNCT_1:12;

then I . (R0 . ((proj (1,1)) . (y - x))) = ((I * R0) * (proj (1,1))) . (y - x) by RELAT_1:36;

then A37: I . (R0 . ((proj (1,1)) . (y - x))) = R /. (y - x) by A36, PARTFUN1:def 6;

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

then y in dom (proj (1,1)) by Lm1, REAL_NS1:def 4;

then A38: I . (g . ((proj (1,1)) . y)) = I . ((g * (proj (1,1))) . y) by FUNCT_1:13;

I . (L0 . ((proj (1,1)) . (y - x))) = I . ((L0 * (proj (1,1))) . (y - x)) by A34, FUNCT_1:13;

then I . (L0 . ((proj (1,1)) . (y - x))) = (I * (L0 * (proj (1,1)))) . (y - x) by A33, FUNCT_1:12;

then A39: I . (L0 . ((proj (1,1)) . (y - x))) = L . (y - x) by RELAT_1:36;

y in dom f by A23, A30;

then y in dom (I * (g * (proj (1,1)))) by A1, RELAT_1:36;

then I . (g . ((proj (1,1)) . y)) = (I * (g * (proj (1,1)))) . y by A38, FUNCT_1:12;

then I . (g . ((proj (1,1)) . y)) = f . y by A1, RELAT_1:36;

then I . (g . ((proj (1,1)) . y)) = f /. y by A23, A30, PARTFUN1:def 6;

then (I . gJy) - (I . gJx) = (f /. y) - (f /. x) by A29, REAL_NS1:5;

hence (f /. y) - (f /. x) = (L . (y - x)) + (R /. (y - x)) by A32, A37, A39, REAL_NS1:2; :: thesis: verum

end;then x in dom (proj (1,1)) by Lm1, REAL_NS1:def 4;

then A27: I . (g . ((proj (1,1)) . x)) = I . ((g * (proj (1,1))) . x) by FUNCT_1:13;

A28: x in { z where z is Point of (REAL-NS 1) : ||.(z - x).|| < e } by A24, NFCONT_1:4;

then x in dom f by A23;

then x in dom (I * (g * (proj (1,1)))) by A1, RELAT_1:36;

then I . (g . ((proj (1,1)) . x)) = (I * (g * (proj (1,1)))) . x by A27, FUNCT_1:12;

then I . (g . ((proj (1,1)) . x)) = f . x by A1, RELAT_1:36;

then A29: I . (g . ((proj (1,1)) . x)) = f /. x by A23, A28, PARTFUN1:def 6;

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

assume A30: y in { z where z is Point of (REAL-NS 1) : ||.(z - x).|| < e } ; :: thesis: (f /. y) - (f /. x) = (L . (y - x)) + (R /. (y - x))

reconsider y0 = (proj (1,1)) . y as Element of REAL by XREAL_0:def 1;

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

reconsider gy0 = g . y0, gx0 = g . x0, g0 = g . 0 as Element of REAL by XREAL_0:def 1;

reconsider L0y0x0 = L0 . y0x0 as Element of REAL by XREAL_0:def 1;

reconsider R0y0x0 = R0 . y0x0, Jyx = (proj (1,1)) . (y - x) as Element of REAL by XREAL_0:def 1;

reconsider gJy = g . ((proj (1,1)) . y), gJx = g . ((proj (1,1)) . x) as Element of REAL by XREAL_0:def 1;

reconsider R0Jyx = R0 . Jyx, L0Jyx = L0 . Jyx as Element of REAL by XREAL_0:def 1;

reconsider p1 = I . gy0, p2 = I . gx0, q1 = I . L0y0x0, q2 = I . R0y0x0 as VECTOR of (REAL-NS 1) by REAL_NS1:def 4;

A31: (proj (1,1)) . x = x0 by A2, Lm1;

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

then y in REAL 1 by REAL_NS1:def 4;

then I . ((g . y0) - (g . x0)) = I . ((L0 . (y0 - x0)) + (R0 . (y0 - x0))) by A10, A25, A30, FUNCT_2:35;

then p1 - p2 = I . ((L0 . (y0 - x0)) + (R0 . (y0 - x0))) by Th3;

then p1 - p2 = q1 + q2 by Th3;

then (I . gy0) - (I . gx0) = q1 + q2 by REAL_NS1:5;

then (I . gJy) - (I . gJx) = (I . L0y0x0) + (I . R0y0x0) by A31, REAL_NS1:2;

then (I . gJy) - (I . gJx) = (I . L0Jyx) + (I . R0y0x0) by A31, Th4;

then A32: (I . gJy) - (I . gJx) = (I . L0Jyx) + (I . R0Jyx) by A31, Th4;

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

then y - x in dom ((I * L0) * (proj (1,1))) ;

then A33: y - x in dom (I * (L0 * (proj (1,1)))) by RELAT_1:36;

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

then A34: y - x in dom (proj (1,1)) by Lm1, REAL_NS1:def 4;

then A35: I . (R0 . ((proj (1,1)) . (y - x))) = I . ((R0 * (proj (1,1))) . (y - x)) by FUNCT_1:13;

R is total by NDIFF_1:def 5;

then A36: dom ((I * R0) * (proj (1,1))) = the carrier of (REAL-NS 1) by PARTFUN1:def 2;

then y - x in dom ((I * R0) * (proj (1,1))) ;

then y - x in dom (I * (R0 * (proj (1,1)))) by RELAT_1:36;

then I . (R0 . ((proj (1,1)) . (y - x))) = (I * (R0 * (proj (1,1)))) . (y - x) by A35, FUNCT_1:12;

then I . (R0 . ((proj (1,1)) . (y - x))) = ((I * R0) * (proj (1,1))) . (y - x) by RELAT_1:36;

then A37: I . (R0 . ((proj (1,1)) . (y - x))) = R /. (y - x) by A36, PARTFUN1:def 6;

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

then y in dom (proj (1,1)) by Lm1, REAL_NS1:def 4;

then A38: I . (g . ((proj (1,1)) . y)) = I . ((g * (proj (1,1))) . y) by FUNCT_1:13;

I . (L0 . ((proj (1,1)) . (y - x))) = I . ((L0 * (proj (1,1))) . (y - x)) by A34, FUNCT_1:13;

then I . (L0 . ((proj (1,1)) . (y - x))) = (I * (L0 * (proj (1,1)))) . (y - x) by A33, FUNCT_1:12;

then A39: I . (L0 . ((proj (1,1)) . (y - x))) = L . (y - x) by RELAT_1:36;

y in dom f by A23, A30;

then y in dom (I * (g * (proj (1,1)))) by A1, RELAT_1:36;

then I . (g . ((proj (1,1)) . y)) = (I * (g * (proj (1,1)))) . y by A38, FUNCT_1:12;

then I . (g . ((proj (1,1)) . y)) = f . y by A1, RELAT_1:36;

then I . (g . ((proj (1,1)) . y)) = f /. y by A23, A30, PARTFUN1:def 6;

then (I . gJy) - (I . gJx) = (f /. y) - (f /. x) by A29, REAL_NS1:5;

hence (f /. y) - (f /. x) = (L . (y - x)) + (R /. (y - x)) by A32, A37, A39, REAL_NS1:2; :: thesis: verum

then A40: dom L0 = REAL by PARTFUN1:def 2;

A41: L is Point of (R_NormSpace_of_BoundedLinearOperators ((REAL-NS 1),(REAL-NS 1))) by LOPBAN_1:def 9;

then f is_differentiable_in x by A24, A23, A26, NDIFF_1:def 6;

then diff (f,x) = (I * L0) * (proj (1,1)) by A24, A23, A41, A26, NDIFF_1:def 7;

then (diff (f,x)) . <*1*> = ((I * L0) * (proj (1,1))) . (I . 1) by Lm1;

then (diff (f,x)) . <*jj*> = (I * L0) . ((proj (1,1)) . (I . jj)) by Lm1, FUNCT_1:13;

then (diff (f,x)) . <*jj*> = I . (L0 . ((proj (1,1)) . (I . jj))) by A40, FUNCT_1:13;

then (diff (f,x)) . <*1*> = I . (L0 . 1) by Lm1, FUNCT_1:35;

hence ( f is_differentiable_in x & (diff (f,x)) . <*1*> = <*(diff (g,y))*> ) by A24, A23, A9, A41, A26, Lm1, NDIFF_1:def 6; :: thesis: verum