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:
set J = proj 1,1;
reconsider L = diff f,x as bounded LinearOperator of (REAL-NS 1),(REAL-NS 1) by LOPBAN_1:def 10;
A1: rng g c= dom I by Th2;
reconsider L0 = ((proj 1,1) * L) * I as LINEAR by Th5;
assume that
A2: f = <>* g and
A3: x = <*y*> and
A4: f is_differentiable_in x ; :: thesis:
consider NN being Neighbourhood of x such that
A5: NN c= dom f and
A6: ex R being REST of (REAL-NS 1),(REAL-NS 1) st
for y being Point of (REAL-NS 1) st y in NN holds
(f /. y) - (f /. x) = ((diff f,x) . (y - x)) + (R /. (y - x)) by A4, NDIFF_1:def 7;
consider e being Real such that
A7: 0 < e and
A8: { z where z is Point of (REAL-NS 1) : ||.(z - x).|| < e } c= NN by NFCONT_1:def 3;
consider R being REST of (REAL-NS 1),(REAL-NS 1) such that
A9: for x9 being Point of (REAL-NS 1) st x9 in NN holds
(f /. x9) - (f /. x) = ((diff f,x) . (x9 - x)) + (R /. (x9 - x)) by A6;
set N = { z where z is Point of (REAL-NS 1) : ||.(z - x).|| < e } ;
A10: { 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 reconsider N = { z where z is Point of (REAL-NS 1) : ||.(z - x).|| < e } as Neighbourhood of x by A7, NFCONT_1:def 3;
set N0 = { z where z is Element of REAL : abs (z - y) < e } ;
A11: N c= dom f by A5, A8, XBOOLE_1:1;

now

let z be set ; :: thesis:

hereby :: thesis:

assume z in { z where z is Element of REAL : abs (z - y) < e } ; :: thesis:
then consider y9 being Element of REAL such that
A12: z = y9 and
A13: abs (y9 - y) < e ;
reconsider w = I . y9 as Point of (REAL-NS 1) by REAL_NS1:def 4;
x = I . y by A3, Lm1;
then w - x = I . (y9 - y) by Th3;
then ||.(w - x).|| = abs (y9 - y) by Th3;
then w in { z0 where z0 is Point of (REAL-NS 1) : ||.(z0 - x).|| < e } by A13;
then (proj 1,1) . w in (proj 1,1) .: N by FUNCT_2:43;
hence z in (proj 1,1) .: N by A12, Lm1, FUNCT_1:57; :: thesis:

end;

assume z in (proj 1,1) .: N ; :: thesis:
then consider ww being set such that
ww in REAL 1 and
A14: ww in N and
A15: z = (proj 1,1) . ww by FUNCT_2:115;
consider w being Point of (REAL-NS 1) such that
A16: ww = w and
A17: ||.(w - x).|| < e by A14;
reconsider y9 = (proj 1,1) . w as Element of REAL ;
(proj 1,1) . x = y by A3, Lm1;
then (proj 1,1) . (w - x) = y9 - y by Th4;
then abs (y9 - y) < e by A17, Th4;
hence z in { z where z is Element of REAL : abs (z - y) < e } by A15, A16; :: thesis:

end;

then A18: { z where z is Element of REAL : abs (z - y) < e } = (proj 1,1) .: N by TARSKI:2;
dom f = (proj 1,1) " (dom (I * g)) by A2, RELAT_1:182;
then (proj 1,1) .: (dom f) = (proj 1,1) .: ((proj 1,1) " (dom g)) by A1, RELAT_1:46;
then A19: (proj 1,1) .: (dom f) = dom g by Lm1, FUNCT_1:147;
A20: I * (proj 1,1) = id (REAL 1) by Lm1, FUNCT_1:61;
reconsider R0 = ((proj 1,1) * R) * I as REST by Th5;
A21: (proj 1,1) * I = id REAL by Lm1, FUNCT_1:61;
N c= dom f by A5, A8, XBOOLE_1:1;
then A22: { z where z is Element of REAL : abs (z - y) < e } c= dom g by A19, A18, RELAT_1:156;
A23: ].(y - e),(y + e).[ c= { z where z is Element of REAL : abs (z - y) < e }

proof

let d be set ; :: according to TARSKI:def 3 :: thesis:
assume A24: d in ].(y - e),(y + e).[ ; :: thesis:
reconsider y0 = d as Element of REAL by A24;
abs (y0 - y) < e by A24, RCOMP_1:8;
hence d in { z where z is Element of REAL : abs (z - y) < e } ; :: thesis:

end;

{ z where z is Element of REAL : abs (z - y) < e } c= ].(y - e),(y + e).[

proof

let d be set ; :: according to TARSKI:def 3 :: thesis:
assume d in { z where z is Element of REAL : abs (z - y) < e } ; :: thesis:
then ex r being Element of REAL st
( d = r & abs (r - y) < e ) ;
hence d in ].(y - e),(y + e).[ by RCOMP_1:8; :: thesis:

end;

then { z where z is Element of REAL : abs (z - y) < e } = ].(y - e),(y + e).[ by A23, XBOOLE_0:def 10;
then A25: { z where z is Element of REAL : abs (z - y) < e } is Neighbourhood of y by A7, RCOMP_1:def 7;
N c= REAL 1 by A10, REAL_NS1:def 4;
then (I * (proj 1,1)) .: N = N by A20, FRECHET:13;
then A26: I .: { z where z is Element of REAL : abs (z - y) < e } = N by A18, RELAT_1:159;
A27: for y0 being Real st y0 in { z where z is Element of REAL : abs (z - y) < e } holds
(g . y0) - (g . y) = (L0 . (y0 - y)) + (R0 . (y0 - y))

proof

let y0 be Real; :: thesis:
reconsider y9 = I . y0 as Point of (REAL-NS 1) by REAL_NS1:def 4;
R is total by NDIFF_1:def 5;
then A28: dom R = the carrier of (REAL-NS 1) by PARTFUN1:def 4;
R0 is total by FDIFF_1:def 3;
then dom (((proj 1,1) * R) * I) = REAL by PARTFUN1:def 4;
then y0 - y in dom (((proj 1,1) * R) * I) ;
then A29: y0 - y in dom ((proj 1,1) * (R * I)) by RELAT_1:55;
I . (y0 - y) in REAL 1 ;
then I . (y0 - y) in dom R by A28, REAL_NS1:def 4;
then (proj 1,1) . (R /. (I . (y0 - y))) = (proj 1,1) . (R . (I . (y0 - y))) by PARTFUN1:def 8;
then (proj 1,1) . (R /. (I . (y0 - y))) = (proj 1,1) . ((R * I) . (y0 - y)) by Th2, FUNCT_1:23;
then (proj 1,1) . (R /. (I . (y0 - y))) = ((proj 1,1) * (R * I)) . (y0 - y) by A29, FUNCT_1:22;
then A30: (proj 1,1) . (R /. (I . (y0 - y))) = R0 . (y0 - y) by RELAT_1:55;
L0 is total by FDIFF_1:def 4;
then dom (((proj 1,1) * L) * I) = REAL by PARTFUN1:def 4;
then y0 - y in dom (((proj 1,1) * L) * I) ;
then A31: y0 - y in dom ((proj 1,1) * (L * I)) by RELAT_1:55;
assume A32: y0 in { z where z is Element of REAL : abs (z - y) < e } ; :: thesis:
then A33: I . y0 in N by A26, FUNCT_2:43;
then (proj 1,1) . (f /. (I . y0)) = (proj 1,1) . (f . (I . y0)) by A11, PARTFUN1:def 8;
then A34: (proj 1,1) . (f /. (I . y0)) = (proj 1,1) . ((f * I) . y0) by Th2, FUNCT_1:23;
(proj 1,1) * f = (proj 1,1) * (I * (g * (proj 1,1))) by A2, RELAT_1:55;
then A35: (proj 1,1) * f = (id REAL ) * (g * (proj 1,1)) by A21, RELAT_1:55;
rng (g * (proj 1,1)) c= REAL ;
then ((proj 1,1) * f) * I = (g * (proj 1,1)) * I by A35, RELAT_1:79;
then A36: ((proj 1,1) * f) * I = g * (id REAL ) by A21, RELAT_1:55;
dom g c= REAL ;
then A37: g = ((proj 1,1) * f) * I by A36, RELAT_1:77;
y0 in dom g by A22, A32;
then y0 in dom ((proj 1,1) * (f * I)) by A37, RELAT_1:55;
then (proj 1,1) . (f /. (I . y0)) = ((proj 1,1) * (f * I)) . y0 by A34, FUNCT_1:22;
then A38: (proj 1,1) . (f /. (I . y0)) = g . y0 by A37, RELAT_1:55;
A39: x = I . y by A3, Lm1;
x in N by NFCONT_1:4;
then (proj 1,1) . (f /. (I . y)) = (proj 1,1) . (f . (I . y)) by A11, A39, PARTFUN1:def 8;
then A40: (proj 1,1) . (f /. (I . y)) = (proj 1,1) . ((f * I) . y) by Th2, FUNCT_1:23;
y in { z where z is Element of REAL : abs (z - y) < e } by A25, RCOMP_1:37;
then y in dom g by A22;
then y in dom ((proj 1,1) * (f * I)) by A37, RELAT_1:55;
then (proj 1,1) . (f /. (I . y)) = ((proj 1,1) * (f * I)) . y by A40, FUNCT_1:22;
then A41: (proj 1,1) . (f /. (I . y)) = g . y by A37, RELAT_1:55;
(proj 1,1) . ((f /. y9) - (f /. x)) = (proj 1,1) . ((L . (y9 - x)) + (R /. (y9 - x))) by A9, A8, A33;
then ((proj 1,1) . (f /. y9)) - ((proj 1,1) . (f /. x)) = (proj 1,1) . ((L . (y9 - x)) + (R /. (y9 - x))) by Th4;
then ((proj 1,1) . (f /. (I . y0))) - ((proj 1,1) . (f /. (I . y))) = ((proj 1,1) . (L . (y9 - x))) + ((proj 1,1) . (R /. (y9 - x))) by A39, Th4;
then A42: ((proj 1,1) . (f /. (I . y0))) - ((proj 1,1) . (f /. (I . y))) = ((proj 1,1) . (L . (I . (y0 - y)))) + ((proj 1,1) . (R /. (y9 - x))) by A39, Th3;
(proj 1,1) . (L . (I . (y0 - y))) = (proj 1,1) . ((L * I) . (y0 - y)) by Th2, FUNCT_1:23;
then (proj 1,1) . (L . (I . (y0 - y))) = ((proj 1,1) * (L * I)) . (y0 - y) by A31, FUNCT_1:22;
then (proj 1,1) . (L . (I . (y0 - y))) = L0 . (y0 - y) by RELAT_1:55;
hence (g . y0) - (g . y) = (L0 . (y0 - y)) + (R0 . (y0 - y)) by A39, A42, A38, A41, A30, Th3; :: thesis:

end;

hence g is_differentiable_in y by A25, A22, FDIFF_1:def 5; :: thesis:
hence diff g,y = (((proj 1,1) * (diff f,x)) * ((proj 1,1) " )) . 1 by A25, A22, A27, FDIFF_1:def 6; :: thesis: