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*> & 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 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 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 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);
reconsider L = diff (f,x) as Lipschitzian LinearOperator of (REAL-NS 1),(REAL-NS 1) by LOPBAN_1:def 9;
A1: rng g c= dom I by Th2;
reconsider L0 = ((proj (1,1)) * L) * I as LinearFunc by Th5;
assume that
A2: f = <>* g and
A3: x = <*y*> and
A4: f is_differentiable_in x ; :: thesis: ( g is_differentiable_in y & diff (g,y) = (((proj (1,1)) * (diff (f,x))) * ((proj (1,1)) ")) . 1 )
consider NN being Neighbourhood of x such that
A5: NN c= dom f and
A6: ex R being RestFunc 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 1;
consider R being RestFunc 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 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;

then reconsider N = { z where z is Point of (REAL-NS 1) : ||.(z - x).|| < e } as Neighbourhood of x by A7, NFCONT_1:def 1;
set N0 = { z where z is Element of REAL : |.(z - y).| < e } ;
A11: N c= dom f by A5, A8;

now :: thesis: for z being object holds
( ( z in { z where z is Element of REAL : |.(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 : |.(z - y).| < e } ) )

let z be object ; :: thesis: ( ( z in { z where z is Element of REAL : |.(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 : |.(z - y).| < e } ) )

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

assume z in { z where z is Element of REAL : |.(z - y).| < e } ; :: thesis: z in (proj (1,1)) .: N
then consider y9 being Element of REAL such that
A12: z = y9 and
A13: |.(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).|| = |.(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:35;
hence z in (proj (1,1)) .: N by A12, Lm1, FUNCT_1:35; :: thesis: verum

end;

assume z in (proj (1,1)) .: N ; :: thesis: z in { z where z is Element of REAL : |.(z - y).| < e }
then consider ww being object such that
ww in REAL 1 and
A14: ww in N and
A15: z = (proj (1,1)) . ww by FUNCT_2:64;
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 by XREAL_0:def 1;
(proj (1,1)) . x = y by A3, Lm1;
then (proj (1,1)) . (w - x) = y9 - y by Th4;
then |.(y9 - y).| < e by A17, Th4;
hence z in { z where z is Element of REAL : |.(z - y).| < e } by A15, A16; :: thesis: verum

end;

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

proof

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

end;

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

proof

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

end;

then { z where z is Element of REAL : |.(z - y).| < e } = ].(y - e),(y + e).[ by A23, XBOOLE_0:def 10;
then A25: { z where z is Element of REAL : |.(z - y).| < e } is Neighbourhood of y by A7, RCOMP_1:def 6;
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 : |.(z - y).| < e } = N by A18, RELAT_1:126;
A27: for y0 being Real st y0 in { z where z is Element of REAL : |.(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 : |.(z - y).| < e } implies (g . y0) - (g . y) = (L0 . (y0 - y)) + (R0 . (y0 - y)) )
reconsider yy0 = y0, yy = y as Element of REAL by XREAL_0:def 1;
reconsider y9 = I . yy0 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 2;
R0 is total by FDIFF_1:def 2;
then dom (((proj (1,1)) * R) * I) = REAL by PARTFUN1:def 2;
then yy0 - yy in dom (((proj (1,1)) * R) * I) ;
then A29: y0 - y in dom ((proj (1,1)) * (R * I)) by RELAT_1:36;
I . (yy0 - yy) in REAL 1 ;
then I . (yy0 - yy) in dom R by A28, REAL_NS1:def 4;
then (proj (1,1)) . (R /. (I . (yy0 - yy))) = (proj (1,1)) . (R . (I . (yy0 - yy))) by PARTFUN1:def 6;
then (proj (1,1)) . (R /. (I . (yy0 - yy))) = (proj (1,1)) . ((R * I) . (yy0 - yy)) by Th2, FUNCT_1:13;
then (proj (1,1)) . (R /. (I . (yy0 - yy))) = ((proj (1,1)) * (R * I)) . (yy0 - yy) by A29, FUNCT_1:12;
then A30: (proj (1,1)) . (R /. (I . (yy0 - yy))) = R0 . (yy0 - yy) by RELAT_1:36;
L0 is total by FDIFF_1:def 3;
then dom (((proj (1,1)) * L) * I) = REAL by PARTFUN1:def 2;
then yy0 - yy in dom (((proj (1,1)) * L) * I) ;
then A31: y0 - y in dom ((proj (1,1)) * (L * I)) by RELAT_1:36;
assume A32: y0 in { z where z is Element of REAL : |.(z - y).| < e } ; :: thesis: (g . y0) - (g . y) = (L0 . (y0 - y)) + (R0 . (y0 - y))
then A33: I . yy0 in N by A26, FUNCT_2:35;
then (proj (1,1)) . (f /. (I . yy0)) = (proj (1,1)) . (f . (I . yy0)) by A11, PARTFUN1:def 6;
then A34: (proj (1,1)) . (f /. (I . yy0)) = (proj (1,1)) . ((f * I) . yy0) by Th2, FUNCT_1:13;
(proj (1,1)) * f = (proj (1,1)) * (I * (g * (proj (1,1)))) by A2, RELAT_1:36;
then A35: (proj (1,1)) * f = (id REAL) * (g * (proj (1,1))) by A21, RELAT_1:36;
rng (g * (proj (1,1))) c= REAL ;
then ((proj (1,1)) * f) * I = (g * (proj (1,1))) * I by A35, RELAT_1:53;
then A36: ((proj (1,1)) * f) * I = g * (id REAL) by A21, RELAT_1:36;
dom g c= REAL ;
then A37: g = ((proj (1,1)) * f) * I by A36, RELAT_1:51;
y0 in dom g by A22, A32;
then y0 in dom ((proj (1,1)) * (f * I)) by A37, RELAT_1:36;
then (proj (1,1)) . (f /. (I . y0)) = ((proj (1,1)) * (f * I)) . y0 by A34, FUNCT_1:12;
then A38: (proj (1,1)) . (f /. (I . y0)) = g . y0 by A37, RELAT_1:36;
A39: x = I . y by A3, Lm1;
set Iy = I . yy;
x in N by NFCONT_1:4;
then (proj (1,1)) . (f /. (I . y)) = (proj (1,1)) . (f . (I . yy)) by A11, A39, PARTFUN1:def 6;
then A40: (proj (1,1)) . (f /. (I . yy)) = (proj (1,1)) . ((f * I) . yy) by Th2, FUNCT_1:13;
y in { z where z is Element of REAL : |.(z - y).| < e } by A25, RCOMP_1:16;
then y in dom g by A22;
then y in dom ((proj (1,1)) * (f * I)) by A37, RELAT_1:36;
then (proj (1,1)) . (f /. (I . y)) = ((proj (1,1)) * (f * I)) . y by A40, FUNCT_1:12;
then A41: (proj (1,1)) . (f /. (I . y)) = g . y by A37, RELAT_1:36;
(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 . (yy0 - yy))) = (proj (1,1)) . ((L * I) . (yy0 - yy)) by Th2, FUNCT_1:13;
then (proj (1,1)) . (L . (I . (y0 - y))) = ((proj (1,1)) * (L * I)) . (y0 - y) by A31, FUNCT_1:12;
then (proj (1,1)) . (L . (I . (y0 - y))) = L0 . (y0 - y) by RELAT_1:36;
hence (g . y0) - (g . y) = (L0 . (y0 - y)) + (R0 . (y0 - y)) by A39, A42, A38, A41, A30, Th3; :: thesis: verum

end;

hence g is_differentiable_in y by A25, A22, FDIFF_1:def 4; :: 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 A25, A22, A27, FDIFF_1:def 5; :: thesis: verum