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 Element of REAL st f = <>* g & x = <*y*> & f is_differentiable_in x holds
( g is_differentiable_in y & diff g,y = (((proj 1,1) * (diff f,x)) * ((proj 1,1) " )) . 1 )
let g be PartFunc of REAL ,REAL ; :: thesis: for x being Point of (REAL-NS 1)
for y being Element of REAL st f = <>* g & x = <*y*> & f is_differentiable_in x holds
( g is_differentiable_in y & diff g,y = (((proj 1,1) * (diff f,x)) * ((proj 1,1) " )) . 1 )
let x be Point of (REAL-NS 1); :: thesis: for y being Element of REAL st f = <>* g & x = <*y*> & f is_differentiable_in x holds
( g is_differentiable_in y & diff g,y = (((proj 1,1) * (diff f,x)) * ((proj 1,1) " )) . 1 )
let y be Element of REAL ; :: thesis: ( f = <>* g & x = <*y*> & f is_differentiable_in x implies ( g is_differentiable_in y & diff g,y = (((proj 1,1) * (diff f,x)) * ((proj 1,1) " )) . 1 ) )
set J = proj 1,1;
assume A1: ( f = <>* g & x = <*y*> & f is_differentiable_in x ) ; :: thesis: ( g is_differentiable_in y & diff g,y = (((proj 1,1) * (diff f,x)) * ((proj 1,1) " )) . 1 )
then consider NN being Neighbourhood of x such that
A2: ( NN c= dom f & 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 NDIFF_1:def 7;
consider R being REST of (REAL-NS 1),(REAL-NS 1) such that
A3: for x' being Point of (REAL-NS 1) st x' in NN holds
(f /. x') - (f /. x) = ((diff f,x) . (x' - x)) + (R /. (x' - x)) by A2;
consider e being Real such that
A4: ( 0 < e & { z where z is Point of (REAL-NS 1) : ||.(z - x).|| < e } c= NN ) by NFCONT_1:def 3;
set N = { z where z is Point of (REAL-NS 1) : ||.(z - x).|| < e } ;
A5: { 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: ( 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;

then reconsider N = { z where z is Point of (REAL-NS 1) : ||.(z - x).|| < e } as Neighbourhood of x by A4, NFCONT_1:def 3;
A6: N c= dom f by A2, A4, XBOOLE_1:1;
set N0 = { z where z is Element of REAL : abs (z - y) < e } ;
A7: { 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: ( not d in { z where z is Element of REAL : abs (z - y) < e } or d in ].(y - e),(y + e).[ )
assume d in { z where z is Element of REAL : abs (z - y) < e } ; :: thesis: d in ].(y - e),(y + e).[
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: verum

end;

].(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: ( not d in ].(y - e),(y + e).[ or d in { z where z is Element of REAL : abs (z - y) < e } )
assume A8: d in ].(y - e),(y + e).[ ; :: thesis: d in { z where z is Element of REAL : abs (z - y) < e }
reconsider y0 = d as Element of REAL by A8;
abs (y0 - y) < e by A8, RCOMP_1:8;
hence d in { z where z is Element of REAL : abs (z - y) < e } ; :: thesis: verum

end;

then { z where z is Element of REAL : abs (z - y) < e } = ].(y - e),(y + e).[ by A7, XBOOLE_0:def 10;
then A9: { z where z is Element of REAL : abs (z - y) < e } is Neighbourhood of y by A4, RCOMP_1:def 7;
( dom f = (proj 1,1) " (dom (I * g)) & rng g c= dom I ) by A1, Th2, RELAT_1:182;
then (proj 1,1) .: (dom f) = (proj 1,1) .: ((proj 1,1) " (dom g)) by RELAT_1:46;
then A10: (proj 1,1) .: (dom f) = dom g by Lm1, FUNCT_1:147;

now

let z be set ; :: thesis: ( ( z in { z where z is Element of REAL : abs (z - y) < e } implies z in (proj 1,1) .: N ) & ( z in (proj 1,1) .: N implies z in { z where z is Element of REAL : abs (z - y) < e } ) )

hereby :: thesis: ( z in (proj 1,1) .: N implies z in { z where z is Element of REAL : abs (z - y) < e } )

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

end;

assume z in (proj 1,1) .: N ; :: thesis: z in { z where z is Element of REAL : abs (z - y) < e }
then consider ww being set such that
A12: ( ww in REAL 1 & ww in N & z = (proj 1,1) . ww ) by FUNCT_2:115;
consider w being Point of (REAL-NS 1) such that
A13: ( ww = w & ||.(w - x).|| < e ) by A12;
reconsider y' = (proj 1,1) . w as Element of REAL ;
(proj 1,1) . x = y by A1, Lm1;
then (proj 1,1) . (w - x) = y' - y by Th4;
then abs (y' - y) < e by A13, Th4;
hence z in { z where z is Element of REAL : abs (z - y) < e } by A12, A13; :: thesis: verum

end;

then A14: { z where z is Element of REAL : abs (z - y) < e } = (proj 1,1) .: N by TARSKI:2;
N c= dom f by A2, A4, XBOOLE_1:1;
then A15: { z where z is Element of REAL : abs (z - y) < e } c= dom g by A10, A14, RELAT_1:156;
reconsider L = diff f,x as bounded LinearOperator of (REAL-NS 1),(REAL-NS 1) by LOPBAN_1:def 10;
reconsider L0 = ((proj 1,1) * L) * I as LINEAR by Th5;
reconsider R0 = ((proj 1,1) * R) * I as REST by Th5;
A16: (proj 1,1) * I = id REAL by Lm1, FUNCT_1:61;
A17: I * (proj 1,1) = id (REAL 1) by Lm1, FUNCT_1:61;
N c= REAL 1 by A5, REAL_NS1:def 4;
then (I * (proj 1,1)) .: N = N by A17, FRECHET:13;
then A18: I .: { z where z is Element of REAL : abs (z - y) < e } = N by A14, RELAT_1:159;
A19: 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: ( y0 in { z where z is Element of REAL : abs (z - y) < e } implies (g . y0) - (g . y) = (L0 . (y0 - y)) + (R0 . (y0 - y)) )
assume A20: y0 in { z where z is Element of REAL : abs (z - y) < e } ; :: thesis: (g . y0) - (g . y) = (L0 . (y0 - y)) + (R0 . (y0 - y))
then A21: I . y0 in N by A18, FUNCT_2:43;
A22: x = I . y by A1, Lm1;
A23: y in { z where z is Element of REAL : abs (z - y) < e } by A9, RCOMP_1:37;
A24: dom g c= REAL ;
A25: 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 A16, RELAT_1:55;
then ((proj 1,1) * f) * I = (g * (proj 1,1)) * I by A25, RELAT_1:79;
then ((proj 1,1) * f) * I = g * (id REAL ) by A16, RELAT_1:55;
then A26: g = ((proj 1,1) * f) * I by A24, RELAT_1:77;
reconsider y' = I . y0 as Point of (REAL-NS 1) by REAL_NS1:def 4;
(proj 1,1) . ((f /. y') - (f /. x)) = (proj 1,1) . ((L . (y' - x)) + (R /. (y' - x))) by A3, A4, A21;
then ((proj 1,1) . (f /. y')) - ((proj 1,1) . (f /. x)) = (proj 1,1) . ((L . (y' - x)) + (R /. (y' - x))) by Th4;
then ((proj 1,1) . (f /. (I . y0))) - ((proj 1,1) . (f /. (I . y))) = ((proj 1,1) . (L . (y' - x))) + ((proj 1,1) . (R /. (y' - x))) by A22, Th4;
then A27: ((proj 1,1) . (f /. (I . y0))) - ((proj 1,1) . (f /. (I . y))) = ((proj 1,1) . (L . (I . (y0 - y)))) + ((proj 1,1) . (R /. (y' - x))) by A22, Th3;
( y0 in dom g & y in dom g ) by A15, A20, A23;
then A28: ( y0 in dom ((proj 1,1) * (f * I)) & y in dom ((proj 1,1) * (f * I)) ) by A26, RELAT_1:55;
x in N by NFCONT_1:4;
then ( (proj 1,1) . (f /. (I . y0)) = (proj 1,1) . (f . (I . y0)) & (proj 1,1) . (f /. (I . y)) = (proj 1,1) . (f . (I . y)) ) by A6, A21, A22, PARTFUN1:def 8;
then ( (proj 1,1) . (f /. (I . y0)) = (proj 1,1) . ((f * I) . y0) & (proj 1,1) . (f /. (I . y)) = (proj 1,1) . ((f * I) . y) ) by Th2, FUNCT_1:23;
then ( (proj 1,1) . (f /. (I . y0)) = ((proj 1,1) * (f * I)) . y0 & (proj 1,1) . (f /. (I . y)) = ((proj 1,1) * (f * I)) . y ) by A28, FUNCT_1:22;
then A29: ( (proj 1,1) . (f /. (I . y0)) = g . y0 & (proj 1,1) . (f /. (I . y)) = g . y ) by A26, 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 A30: y0 - y in dom ((proj 1,1) * (L * I)) by RELAT_1:55;
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 A31: y0 - y in dom ((proj 1,1) * (R * I)) by RELAT_1:55;
R is total by NDIFF_1:def 5;
then A32: dom R = the carrier of (REAL-NS 1) by PARTFUN1:def 4;
I . (y0 - y) in REAL 1 ;
then I . (y0 - y) in dom R by A32, 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 A31, FUNCT_1:22;
then A33: (proj 1,1) . (R /. (I . (y0 - y))) = R0 . (y0 - y) by RELAT_1:55;
(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 A30, 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 A22, A27, A29, A33, Th3; :: thesis: verum

end;

hence g is_differentiable_in y by A9, A15, FDIFF_1:def 5; :: thesis: diff g,y = (((proj 1,1) * (diff f,x)) * ((proj 1,1) " )) . 1
hence diff g,y = (((proj 1,1) * (diff f,x)) * ((proj 1,1) " )) . 1 by A9, A15, A19, FDIFF_1:def 6; :: thesis: verum