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)

set N0 = { z where z is Element of REAL : |.(z - y).| < e } ;

A11: N c= dom f by A5, A8;

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 }

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))

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

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

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;
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

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 } ) )

then A18:
{ z where z is Element of REAL : |.(z - y).| < e } = (proj (1,1)) .: N
by TARSKI:2;( ( 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 } ) )

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

assume
z in (proj (1,1)) .: N
; :: thesis: 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;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

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

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

{ z where z is Element of REAL : |.(z - y).| < e } c= ].(y - e),(y + e).[
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;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

proof

then
{ z where z is Element of REAL : |.(z - y).| < e } = ].(y - e),(y + e).[
by A23, XBOOLE_0:def 10;
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;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

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

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
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;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

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