let f be PartFunc of (REAL-NS 1),(REAL-NS 1); :: thesis:
let g be PartFunc of REAL , REAL ; :: thesis:
let x be Point of (REAL-NS 1); :: thesis:
let y be Element of REAL ; :: thesis:
assume A1: ( f = <>* g & x = <*y*> & g is_differentiable_in y ) ; :: thesis:
reconsider x0 = y as Real ;
set J = proj 1,1;
consider N0 being Neighbourhood of x0 such that
A2: ( N0 c= dom g & ex L0 being LINEAR ex R0 being REST 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 A1, FDIFF_1:def 6;
consider e0 being real number such that
A3: ( 0 < e0 & N0 = ].(x0 - e0),(x0 + e0).[ ) by RCOMP_1:def 7;
reconsider e = e0 as Real by XREAL_0:def 1;
set N = { z where z is Point of (REAL-NS 1) : ||.(z - x).|| < e } ;
{ z where z is Point of (REAL-NS 1) : ||.(z - x).|| < e } c= the carrier of (REAL-NS 1)

proof

let y be set ; :: according to TARSKI:def 3 :: thesis:
assume y in { z where z is Point of (REAL-NS 1) : ||.(z - x).|| < e } ; :: thesis:
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:

end;

then A4: { z where z is Point of (REAL-NS 1) : ||.(z - x).|| < e } is Neighbourhood of x by A3, NFCONT_1:def 3;
A5: (proj 1,1) * I = id REAL by Lm1, FUNCT_1:61;
A6: dom g c= REAL ;
A7: rng (g * (proj 1,1)) c= REAL ;
(proj 1,1) * f = (proj 1,1) * (I * (g * (proj 1,1))) by A1, RELAT_1:55;
then (proj 1,1) * f = (id REAL ) * (g * (proj 1,1)) by A5, RELAT_1:55;
then ((proj 1,1) * f) * I = (g * (proj 1,1)) * I by A7, RELAT_1:79;
then ((proj 1,1) * f) * I = g * (id REAL ) by A5, RELAT_1:55;
then g = ((proj 1,1) * f) * I by A6, RELAT_1:77;
then A8: dom g = I " (dom ((proj 1,1) * f)) by RELAT_1:182;
rng f c= the carrier of (REAL-NS 1) ;
then rng f c= dom (proj 1,1) by Lm1, REAL_NS1:def 4;
then A9: I .: (dom g) = I .: (I " (dom f)) by A8, RELAT_1:46;
dom f c= the carrier of (REAL-NS 1) ;
then dom f c= rng I by Th2, REAL_NS1:def 4;
then A10: I .: (dom g) = dom f by A9, FUNCT_1:147;
A11: { z where z is Point of (REAL-NS 1) : ||.(z - x).|| < e } = I .: N0

proof

now

let z be set ; :: thesis:

hereby :: thesis:

assume z in { z where z is Point of (REAL-NS 1) : ||.(z - x).|| < e } ; :: thesis:
then consider w being Point of (REAL-NS 1) such that
A12: ( z = w & ||.(w - x).|| < e ) ;
reconsider y = (proj 1,1) . w as Element of REAL ;
(proj 1,1) . x = x0 by A1, Lm1;
then (proj 1,1) . (w - x) = y - x0 by Th4;
then abs (y - x0) < e by A12, Th4;
then A13: y in N0 by A3, RCOMP_1:8;
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:56;
hence z in I .: N0 by A12, A13, FUNCT_2:43; :: thesis:

end;

assume z in I .: N0 ; :: thesis:
then consider yy being set such that
A14: ( yy in REAL & yy in N0 & z = I . yy ) by FUNCT_2:115;
reconsider y = yy as Element of REAL by A14;
A15: abs (y - x0) < e by A3, A14, RCOMP_1:8;
reconsider w = I . y as Point of (REAL-NS 1) by REAL_NS1:def 4;
I . x0 = x by A1, Lm1;
then w - x = I . (y - x0) by Th3;
then ||.(w - x).|| < e by A15, Th3;
hence z in { z where z is Point of (REAL-NS 1) : ||.(z - x).|| < e } by A14; :: thesis:

end;

hence { z where z is Point of (REAL-NS 1) : ||.(z - x).|| < e } = I .: N0 by TARSKI:2; :: thesis:

end;

then A16: { z where z is Point of (REAL-NS 1) : ||.(z - x).|| < e } c= dom f by A2, A10, RELAT_1:156;
consider L0 being LINEAR, R0 being REST such that
A17: ( 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 A2;
reconsider L = (I * L0) * (proj 1,1) as bounded LinearOperator of (REAL-NS 1),(REAL-NS 1) by Th6;
A18: L is Point of (R_NormSpace_of_BoundedLinearOperators (REAL-NS 1),(REAL-NS 1)) by LOPBAN_1:def 10;
reconsider R = (I * R0) * (proj 1,1) as REST of (REAL-NS 1),(REAL-NS 1) by Th6;
(proj 1,1) * I = id REAL by Lm1, FUNCT_1:61;
then ((proj 1,1) * I) .: N0 = N0 by FRECHET:13;
then A19: (proj 1,1) .: { z where z is Point of (REAL-NS 1) : ||.(z - x).|| < e } = N0 by A11, RELAT_1:159;
A20: 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

let y be Point of (REAL-NS 1); :: thesis:
assume A21: y in { z where z is Point of (REAL-NS 1) : ||.(z - x).|| < e } ; :: thesis:
A22: x in { z where z is Point of (REAL-NS 1) : ||.(z - x).|| < e } by A4, NFCONT_1:4;
y in the carrier of (REAL-NS 1) ;
then A23: y in REAL 1 by REAL_NS1:def 4;
A24: (proj 1,1) . x = x0 by A1, Lm1;
reconsider y0 = (proj 1,1) . y as Element of REAL ;
reconsider p1 = I . (g . y0), p2 = I . (g . x0), q1 = I . (L0 . (y0 - x0)), q2 = I . (R0 . (y0 - x0)) as VECTOR of (REAL-NS 1) by REAL_NS1:def 4;
I . ((g . y0) - (g . x0)) = I . ((L0 . (y0 - x0)) + (R0 . (y0 - x0))) by A17, A19, A21, A23, FUNCT_2:43;
then p1 - p2 = I . ((L0 . (y0 - x0)) + (R0 . (y0 - x0))) by Th3;
then p1 - p2 = q1 + q2 by Th3;
then (I . (g . y0)) - (I . (g . x0)) = q1 + q2 by REAL_NS1:5;
then (I . (g . ((proj 1,1) . y))) - (I . (g . ((proj 1,1) . x))) = (I . (L0 . (y0 - x0))) + (I . (R0 . (y0 - x0))) by A24, REAL_NS1:2;
then (I . (g . ((proj 1,1) . y))) - (I . (g . ((proj 1,1) . x))) = (I . (L0 . ((proj 1,1) . (y - x)))) + (I . (R0 . (y0 - x0))) by A24, Th4;
then A25: (I . (g . ((proj 1,1) . y))) - (I . (g . ((proj 1,1) . x))) = (I . (L0 . ((proj 1,1) . (y - x)))) + (I . (R0 . ((proj 1,1) . (y - x)))) by A24, Th4;
( y in dom f & x in dom f ) by A16, A21, A22;
then A26: ( y in dom (I * (g * (proj 1,1))) & x in dom (I * (g * (proj 1,1))) ) by A1, RELAT_1:55;
( y in the carrier of (REAL-NS 1) & x in the carrier of (REAL-NS 1) ) ;
then ( y in dom (proj 1,1) & x in dom (proj 1,1) ) by Lm1, REAL_NS1:def 4;
then ( I . (g . ((proj 1,1) . y)) = I . ((g * (proj 1,1)) . y) & I . (g . ((proj 1,1) . x)) = I . ((g * (proj 1,1)) . x) ) by FUNCT_1:23;
then ( I . (g . ((proj 1,1) . y)) = (I * (g * (proj 1,1))) . y & I . (g . ((proj 1,1) . x)) = (I * (g * (proj 1,1))) . x ) by A26, FUNCT_1:22;
then ( I . (g . ((proj 1,1) . y)) = f . y & I . (g . ((proj 1,1) . x)) = f . x ) by A1, RELAT_1:55;
then ( I . (g . ((proj 1,1) . y)) = f /. y & I . (g . ((proj 1,1) . x)) = f /. x ) by A16, A21, A22, PARTFUN1:def 8;
then A27: (I . (g . ((proj 1,1) . y))) - (I . (g . ((proj 1,1) . x))) = (f /. y) - (f /. x) by REAL_NS1:5;
dom L = the carrier of (REAL-NS 1) by FUNCT_2:def 1;
then y - x in dom ((I * L0) * (proj 1,1)) ;
then A28: y - x in dom (I * (L0 * (proj 1,1))) by RELAT_1:55;
R is total by NDIFF_1:def 5;
then A29: dom ((I * R0) * (proj 1,1)) = the carrier of (REAL-NS 1) by PARTFUN1:def 4;
then y - x in dom ((I * R0) * (proj 1,1)) ;
then A30: y - x in dom (I * (R0 * (proj 1,1))) by RELAT_1:55;
y - x in the carrier of (REAL-NS 1) ;
then A31: y - x in dom (proj 1,1) by Lm1, REAL_NS1:def 4;
then I . (R0 . ((proj 1,1) . (y - x))) = I . ((R0 * (proj 1,1)) . (y - x)) by FUNCT_1:23;
then I . (R0 . ((proj 1,1) . (y - x))) = (I * (R0 * (proj 1,1))) . (y - x) by A30, FUNCT_1:22;
then I . (R0 . ((proj 1,1) . (y - x))) = ((I * R0) * (proj 1,1)) . (y - x) by RELAT_1:55;
then A32: I . (R0 . ((proj 1,1) . (y - x))) = R /. (y - x) by A29, PARTFUN1:def 8;
I . (L0 . ((proj 1,1) . (y - x))) = I . ((L0 * (proj 1,1)) . (y - x)) by A31, FUNCT_1:23;
then I . (L0 . ((proj 1,1) . (y - x))) = (I * (L0 * (proj 1,1))) . (y - x) by A28, FUNCT_1:22;
then I . (L0 . ((proj 1,1) . (y - x))) = L . (y - x) by RELAT_1:55;
hence (f /. y) - (f /. x) = (L . (y - x)) + (R /. (y - x)) by A25, A27, A32, REAL_NS1:2; :: thesis:

end;

then f is_differentiable_in x by A4, A16, A18, NDIFF_1:def 6;
then diff f,x = (I * L0) * (proj 1,1) by A4, A16, A18, A20, NDIFF_1:def 7;
then (diff f,x) . <*1*> = ((I * L0) * (proj 1,1)) . (I . 1) by Lm1;
then A33: (diff f,x) . <*1*> = (I * L0) . ((proj 1,1) . (I . 1)) by Lm1, FUNCT_1:23;
L0 is total by FDIFF_1:def 4;
then dom L0 = REAL by PARTFUN1:def 4;
then (diff f,x) . <*1*> = I . (L0 . ((proj 1,1) . (I . 1))) by A33, FUNCT_1:23;
then (diff f,x) . <*1*> = I . (L0 . 1) by Lm1, FUNCT_1:57;
hence ( f is_differentiable_in x & (diff f,x) . <*1*> = <*(diff g,y)*> ) by A4, A16, A17, A18, A20, Lm1, NDIFF_1:def 6; :: thesis: